"""
Copyright 2013 Steven Diamond

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
"""

import ncvx

import cvxpy as cp

from ..extensions.mixed_integer.boolean import Boolean

bv = [] # Boolean variables.
for i in range(26):
	var_row = []
	for j in range(31):
		var_row.append(Boolean())
	bv.append(var_row)



obj = bv[1][24]+bv[2][5]+bv[2][6]+bv[2][7]+bv[2][23]+bv[2][24]+bv[3][5]+bv[3][7]+bv[3][8]+bv[3][22]+bv[3][25]+bv[4][4]+bv[4][8]+bv[4][9]+bv[4][13]+bv[4][14]+bv[4][15]+bv[4][16]+bv[4][17]+bv[4][18]+bv[4][19]+bv[4][22]+bv[4][25]+bv[5][4]+bv[5][6]+bv[5][9]+bv[5][10]+bv[5][11]+bv[5][12]+bv[5][20]+bv[5][21]+bv[5][22]+bv[5][26]+bv[6][4]+bv[6][6]+bv[6][9]+bv[6][22]+bv[6][24]+bv[6][26]+bv[7][4]+bv[7][6]+bv[7][9]+bv[7][22]+bv[7][24]+bv[7][26]+bv[8][4]+bv[8][22]+bv[8][26]+bv[9][4]+bv[9][23]+bv[9][26]+bv[10][5]+bv[10][25]+bv[10][27]+bv[11][6]+bv[11][27]+bv[12][6]+bv[12][9]+bv[12][10]+bv[12][11]+bv[12][19]+bv[12][20]+bv[12][21]+bv[12][27]+bv[13][6]+bv[13][8]+bv[13][12]+bv[13][18]+bv[13][22]+bv[13][27]+bv[14][1]+bv[14][2]+bv[14][5]+bv[14][8]+bv[14][9]+bv[14][10]+bv[14][12]+bv[14][18]+bv[14][19]+bv[14][20]+bv[14][22]+bv[14][28]+bv[15][3]+bv[15][4]+bv[15][5]+bv[15][8]+bv[15][9]+bv[15][10]+bv[15][11]+bv[15][12]+bv[15][19]+bv[15][20]+bv[15][21]+bv[15][28]+bv[16][5]+bv[16][6]+bv[16][14]+bv[16][16]+bv[16][28]+bv[17][1]+bv[17][2]+bv[17][3]+bv[17][4]+bv[17][14]+bv[17][16]+bv[17][27]+bv[17][28]+bv[17][29]+bv[17][30]+bv[18][4]+bv[18][5]+bv[18][6]+bv[18][7]+bv[18][13]+bv[18][16]+bv[18][23]+bv[18][24]+bv[18][25]+bv[18][26]+bv[18][28]+bv[19][4]+bv[19][14]+bv[19][15]+bv[19][28]+bv[20][5]+bv[20][9]+bv[20][10]+bv[20][22]+bv[20][23]+bv[20][24]+bv[20][25]+bv[20][26]+bv[20][27]+bv[20][28]+bv[20][29]+bv[20][30]+bv[21][6]+bv[21][10]+bv[21][11]+bv[21][12]+bv[21][13]+bv[21][14]+bv[21][27]+bv[22][7]+bv[22][8]+bv[22][12]+bv[22][13]+bv[22][14]+bv[22][15]+bv[22][16]+bv[22][17]+bv[22][18]+bv[22][19]+bv[22][20]+bv[22][21]+bv[22][22]+bv[22][26]+bv[23][9]+bv[23][10]+bv[23][13]+bv[23][14]+bv[23][15]+bv[23][16]+bv[23][17]+bv[23][18]+bv[23][19]+bv[23][24]+bv[23][25]+bv[24][11]+bv[24][21]+bv[24][22]+bv[24][23]+bv[25][12]+bv[25][13]+bv[25][14]+bv[25][15]+bv[25][16]+bv[25][17]+bv[25][18]+bv[25][19]+bv[25][20]+bv[25][21]

constraints = [
bv[1][1]+bv[1][2]+bv[1][3]+bv[1][4]+bv[1][5]+bv[1][6]+bv[1][7]+bv[1][8]+bv[1][9]+bv[1][10]+bv[1][11]+bv[1][12]+bv[1][13]+bv[1][14]+bv[1][15]+bv[1][16]+bv[1][17]+bv[1][18]+bv[1][19]+bv[1][20]+bv[1][21]+bv[1][22]+bv[1][23]+bv[1][24]+bv[1][25]+bv[1][26]+bv[1][27]+bv[1][28]+bv[1][29]+bv[1][30] == 1,
bv[2][1]+bv[2][2]+bv[2][3]+bv[2][4]+bv[2][5]+bv[2][6]+bv[2][7]+bv[2][8]+bv[2][9]+bv[2][10]+bv[2][11]+bv[2][12]+bv[2][13]+bv[2][14]+bv[2][15]+bv[2][16]+bv[2][17]+bv[2][18]+bv[2][19]+bv[2][20]+bv[2][21]+bv[2][22]+bv[2][23]+bv[2][24]+bv[2][25]+bv[2][26]+bv[2][27]+bv[2][28]+bv[2][29]+bv[2][30] == 5,
bv[3][1]+bv[3][2]+bv[3][3]+bv[3][4]+bv[3][5]+bv[3][6]+bv[3][7]+bv[3][8]+bv[3][9]+bv[3][10]+bv[3][11]+bv[3][12]+bv[3][13]+bv[3][14]+bv[3][15]+bv[3][16]+bv[3][17]+bv[3][18]+bv[3][19]+bv[3][20]+bv[3][21]+bv[3][22]+bv[3][23]+bv[3][24]+bv[3][25]+bv[3][26]+bv[3][27]+bv[3][28]+bv[3][29]+bv[3][30] == 5,
bv[4][1]+bv[4][2]+bv[4][3]+bv[4][4]+bv[4][5]+bv[4][6]+bv[4][7]+bv[4][8]+bv[4][9]+bv[4][10]+bv[4][11]+bv[4][12]+bv[4][13]+bv[4][14]+bv[4][15]+bv[4][16]+bv[4][17]+bv[4][18]+bv[4][19]+bv[4][20]+bv[4][21]+bv[4][22]+bv[4][23]+bv[4][24]+bv[4][25]+bv[4][26]+bv[4][27]+bv[4][28]+bv[4][29]+bv[4][30] == 12,
bv[5][1]+bv[5][2]+bv[5][3]+bv[5][4]+bv[5][5]+bv[5][6]+bv[5][7]+bv[5][8]+bv[5][9]+bv[5][10]+bv[5][11]+bv[5][12]+bv[5][13]+bv[5][14]+bv[5][15]+bv[5][16]+bv[5][17]+bv[5][18]+bv[5][19]+bv[5][20]+bv[5][21]+bv[5][22]+bv[5][23]+bv[5][24]+bv[5][25]+bv[5][26]+bv[5][27]+bv[5][28]+bv[5][29]+bv[5][30] == 10,
bv[6][1]+bv[6][2]+bv[6][3]+bv[6][4]+bv[6][5]+bv[6][6]+bv[6][7]+bv[6][8]+bv[6][9]+bv[6][10]+bv[6][11]+bv[6][12]+bv[6][13]+bv[6][14]+bv[6][15]+bv[6][16]+bv[6][17]+bv[6][18]+bv[6][19]+bv[6][20]+bv[6][21]+bv[6][22]+bv[6][23]+bv[6][24]+bv[6][25]+bv[6][26]+bv[6][27]+bv[6][28]+bv[6][29]+bv[6][30] == 6,
bv[7][1]+bv[7][2]+bv[7][3]+bv[7][4]+bv[7][5]+bv[7][6]+bv[7][7]+bv[7][8]+bv[7][9]+bv[7][10]+bv[7][11]+bv[7][12]+bv[7][13]+bv[7][14]+bv[7][15]+bv[7][16]+bv[7][17]+bv[7][18]+bv[7][19]+bv[7][20]+bv[7][21]+bv[7][22]+bv[7][23]+bv[7][24]+bv[7][25]+bv[7][26]+bv[7][27]+bv[7][28]+bv[7][29]+bv[7][30] == 6,
bv[8][1]+bv[8][2]+bv[8][3]+bv[8][4]+bv[8][5]+bv[8][6]+bv[8][7]+bv[8][8]+bv[8][9]+bv[8][10]+bv[8][11]+bv[8][12]+bv[8][13]+bv[8][14]+bv[8][15]+bv[8][16]+bv[8][17]+bv[8][18]+bv[8][19]+bv[8][20]+bv[8][21]+bv[8][22]+bv[8][23]+bv[8][24]+bv[8][25]+bv[8][26]+bv[8][27]+bv[8][28]+bv[8][29]+bv[8][30] == 3,
bv[9][1]+bv[9][2]+bv[9][3]+bv[9][4]+bv[9][5]+bv[9][6]+bv[9][7]+bv[9][8]+bv[9][9]+bv[9][10]+bv[9][11]+bv[9][12]+bv[9][13]+bv[9][14]+bv[9][15]+bv[9][16]+bv[9][17]+bv[9][18]+bv[9][19]+bv[9][20]+bv[9][21]+bv[9][22]+bv[9][23]+bv[9][24]+bv[9][25]+bv[9][26]+bv[9][27]+bv[9][28]+bv[9][29]+bv[9][30] == 3,
bv[10][1]+bv[10][2]+bv[10][3]+bv[10][4]+bv[10][5]+bv[10][6]+bv[10][7]+bv[10][8]+bv[10][9]+bv[10][10]+bv[10][11]+bv[10][12]+bv[10][13]+bv[10][14]+bv[10][15]+bv[10][16]+bv[10][17]+bv[10][18]+bv[10][19]+bv[10][20]+bv[10][21]+bv[10][22]+bv[10][23]+bv[10][24]+bv[10][25]+bv[10][26]+bv[10][27]+bv[10][28]+bv[10][29]+bv[10][30] == 3,
bv[11][1]+bv[11][2]+bv[11][3]+bv[11][4]+bv[11][5]+bv[11][6]+bv[11][7]+bv[11][8]+bv[11][9]+bv[11][10]+bv[11][11]+bv[11][12]+bv[11][13]+bv[11][14]+bv[11][15]+bv[11][16]+bv[11][17]+bv[11][18]+bv[11][19]+bv[11][20]+bv[11][21]+bv[11][22]+bv[11][23]+bv[11][24]+bv[11][25]+bv[11][26]+bv[11][27]+bv[11][28]+bv[11][29]+bv[11][30] == 2,
bv[12][1]+bv[12][2]+bv[12][3]+bv[12][4]+bv[12][5]+bv[12][6]+bv[12][7]+bv[12][8]+bv[12][9]+bv[12][10]+bv[12][11]+bv[12][12]+bv[12][13]+bv[12][14]+bv[12][15]+bv[12][16]+bv[12][17]+bv[12][18]+bv[12][19]+bv[12][20]+bv[12][21]+bv[12][22]+bv[12][23]+bv[12][24]+bv[12][25]+bv[12][26]+bv[12][27]+bv[12][28]+bv[12][29]+bv[12][30] == 8,
bv[13][1]+bv[13][2]+bv[13][3]+bv[13][4]+bv[13][5]+bv[13][6]+bv[13][7]+bv[13][8]+bv[13][9]+bv[13][10]+bv[13][11]+bv[13][12]+bv[13][13]+bv[13][14]+bv[13][15]+bv[13][16]+bv[13][17]+bv[13][18]+bv[13][19]+bv[13][20]+bv[13][21]+bv[13][22]+bv[13][23]+bv[13][24]+bv[13][25]+bv[13][26]+bv[13][27]+bv[13][28]+bv[13][29]+bv[13][30] == 6,
bv[14][1]+bv[14][2]+bv[14][3]+bv[14][4]+bv[14][5]+bv[14][6]+bv[14][7]+bv[14][8]+bv[14][9]+bv[14][10]+bv[14][11]+bv[14][12]+bv[14][13]+bv[14][14]+bv[14][15]+bv[14][16]+bv[14][17]+bv[14][18]+bv[14][19]+bv[14][20]+bv[14][21]+bv[14][22]+bv[14][23]+bv[14][24]+bv[14][25]+bv[14][26]+bv[14][27]+bv[14][28]+bv[14][29]+bv[14][30] == 12,
bv[15][1]+bv[15][2]+bv[15][3]+bv[15][4]+bv[15][5]+bv[15][6]+bv[15][7]+bv[15][8]+bv[15][9]+bv[15][10]+bv[15][11]+bv[15][12]+bv[15][13]+bv[15][14]+bv[15][15]+bv[15][16]+bv[15][17]+bv[15][18]+bv[15][19]+bv[15][20]+bv[15][21]+bv[15][22]+bv[15][23]+bv[15][24]+bv[15][25]+bv[15][26]+bv[15][27]+bv[15][28]+bv[15][29]+bv[15][30] == 12,
bv[16][1]+bv[16][2]+bv[16][3]+bv[16][4]+bv[16][5]+bv[16][6]+bv[16][7]+bv[16][8]+bv[16][9]+bv[16][10]+bv[16][11]+bv[16][12]+bv[16][13]+bv[16][14]+bv[16][15]+bv[16][16]+bv[16][17]+bv[16][18]+bv[16][19]+bv[16][20]+bv[16][21]+bv[16][22]+bv[16][23]+bv[16][24]+bv[16][25]+bv[16][26]+bv[16][27]+bv[16][28]+bv[16][29]+bv[16][30] == 5,
bv[17][1]+bv[17][2]+bv[17][3]+bv[17][4]+bv[17][5]+bv[17][6]+bv[17][7]+bv[17][8]+bv[17][9]+bv[17][10]+bv[17][11]+bv[17][12]+bv[17][13]+bv[17][14]+bv[17][15]+bv[17][16]+bv[17][17]+bv[17][18]+bv[17][19]+bv[17][20]+bv[17][21]+bv[17][22]+bv[17][23]+bv[17][24]+bv[17][25]+bv[17][26]+bv[17][27]+bv[17][28]+bv[17][29]+bv[17][30] == 10,
bv[18][1]+bv[18][2]+bv[18][3]+bv[18][4]+bv[18][5]+bv[18][6]+bv[18][7]+bv[18][8]+bv[18][9]+bv[18][10]+bv[18][11]+bv[18][12]+bv[18][13]+bv[18][14]+bv[18][15]+bv[18][16]+bv[18][17]+bv[18][18]+bv[18][19]+bv[18][20]+bv[18][21]+bv[18][22]+bv[18][23]+bv[18][24]+bv[18][25]+bv[18][26]+bv[18][27]+bv[18][28]+bv[18][29]+bv[18][30] == 11,
bv[19][1]+bv[19][2]+bv[19][3]+bv[19][4]+bv[19][5]+bv[19][6]+bv[19][7]+bv[19][8]+bv[19][9]+bv[19][10]+bv[19][11]+bv[19][12]+bv[19][13]+bv[19][14]+bv[19][15]+bv[19][16]+bv[19][17]+bv[19][18]+bv[19][19]+bv[19][20]+bv[19][21]+bv[19][22]+bv[19][23]+bv[19][24]+bv[19][25]+bv[19][26]+bv[19][27]+bv[19][28]+bv[19][29]+bv[19][30] == 4,
bv[20][1]+bv[20][2]+bv[20][3]+bv[20][4]+bv[20][5]+bv[20][6]+bv[20][7]+bv[20][8]+bv[20][9]+bv[20][10]+bv[20][11]+bv[20][12]+bv[20][13]+bv[20][14]+bv[20][15]+bv[20][16]+bv[20][17]+bv[20][18]+bv[20][19]+bv[20][20]+bv[20][21]+bv[20][22]+bv[20][23]+bv[20][24]+bv[20][25]+bv[20][26]+bv[20][27]+bv[20][28]+bv[20][29]+bv[20][30] == 12,
bv[21][1]+bv[21][2]+bv[21][3]+bv[21][4]+bv[21][5]+bv[21][6]+bv[21][7]+bv[21][8]+bv[21][9]+bv[21][10]+bv[21][11]+bv[21][12]+bv[21][13]+bv[21][14]+bv[21][15]+bv[21][16]+bv[21][17]+bv[21][18]+bv[21][19]+bv[21][20]+bv[21][21]+bv[21][22]+bv[21][23]+bv[21][24]+bv[21][25]+bv[21][26]+bv[21][27]+bv[21][28]+bv[21][29]+bv[21][30] == 7,
bv[22][1]+bv[22][2]+bv[22][3]+bv[22][4]+bv[22][5]+bv[22][6]+bv[22][7]+bv[22][8]+bv[22][9]+bv[22][10]+bv[22][11]+bv[22][12]+bv[22][13]+bv[22][14]+bv[22][15]+bv[22][16]+bv[22][17]+bv[22][18]+bv[22][19]+bv[22][20]+bv[22][21]+bv[22][22]+bv[22][23]+bv[22][24]+bv[22][25]+bv[22][26]+bv[22][27]+bv[22][28]+bv[22][29]+bv[22][30] == 14,
bv[23][1]+bv[23][2]+bv[23][3]+bv[23][4]+bv[23][5]+bv[23][6]+bv[23][7]+bv[23][8]+bv[23][9]+bv[23][10]+bv[23][11]+bv[23][12]+bv[23][13]+bv[23][14]+bv[23][15]+bv[23][16]+bv[23][17]+bv[23][18]+bv[23][19]+bv[23][20]+bv[23][21]+bv[23][22]+bv[23][23]+bv[23][24]+bv[23][25]+bv[23][26]+bv[23][27]+bv[23][28]+bv[23][29]+bv[23][30] == 11,
bv[24][1]+bv[24][2]+bv[24][3]+bv[24][4]+bv[24][5]+bv[24][6]+bv[24][7]+bv[24][8]+bv[24][9]+bv[24][10]+bv[24][11]+bv[24][12]+bv[24][13]+bv[24][14]+bv[24][15]+bv[24][16]+bv[24][17]+bv[24][18]+bv[24][19]+bv[24][20]+bv[24][21]+bv[24][22]+bv[24][23]+bv[24][24]+bv[24][25]+bv[24][26]+bv[24][27]+bv[24][28]+bv[24][29]+bv[24][30] == 4,
bv[25][1]+bv[25][2]+bv[25][3]+bv[25][4]+bv[25][5]+bv[25][6]+bv[25][7]+bv[25][8]+bv[25][9]+bv[25][10]+bv[25][11]+bv[25][12]+bv[25][13]+bv[25][14]+bv[25][15]+bv[25][16]+bv[25][17]+bv[25][18]+bv[25][19]+bv[25][20]+bv[25][21]+bv[25][22]+bv[25][23]+bv[25][24]+bv[25][25]+bv[25][26]+bv[25][27]+bv[25][28]+bv[25][29]+bv[25][30] == 10,
bv[1][1]+bv[2][1]+bv[3][1]+bv[4][1]+bv[5][1]+bv[6][1]+bv[7][1]+bv[8][1]+bv[9][1]+bv[10][1]+bv[11][1]+bv[12][1]+bv[13][1]+bv[14][1]+bv[15][1]+bv[16][1]+bv[17][1]+bv[18][1]+bv[19][1]+bv[20][1]+bv[21][1]+bv[22][1]+bv[23][1]+bv[24][1]+bv[25][1] == 2,
bv[1][2]+bv[2][2]+bv[3][2]+bv[4][2]+bv[5][2]+bv[6][2]+bv[7][2]+bv[8][2]+bv[9][2]+bv[10][2]+bv[11][2]+bv[12][2]+bv[13][2]+bv[14][2]+bv[15][2]+bv[16][2]+bv[17][2]+bv[18][2]+bv[19][2]+bv[20][2]+bv[21][2]+bv[22][2]+bv[23][2]+bv[24][2]+bv[25][2] == 2,
bv[1][3]+bv[2][3]+bv[3][3]+bv[4][3]+bv[5][3]+bv[6][3]+bv[7][3]+bv[8][3]+bv[9][3]+bv[10][3]+bv[11][3]+bv[12][3]+bv[13][3]+bv[14][3]+bv[15][3]+bv[16][3]+bv[17][3]+bv[18][3]+bv[19][3]+bv[20][3]+bv[21][3]+bv[22][3]+bv[23][3]+bv[24][3]+bv[25][3] == 2,
bv[1][4]+bv[2][4]+bv[3][4]+bv[4][4]+bv[5][4]+bv[6][4]+bv[7][4]+bv[8][4]+bv[9][4]+bv[10][4]+bv[11][4]+bv[12][4]+bv[13][4]+bv[14][4]+bv[15][4]+bv[16][4]+bv[17][4]+bv[18][4]+bv[19][4]+bv[20][4]+bv[21][4]+bv[22][4]+bv[23][4]+bv[24][4]+bv[25][4] == 10,
bv[1][5]+bv[2][5]+bv[3][5]+bv[4][5]+bv[5][5]+bv[6][5]+bv[7][5]+bv[8][5]+bv[9][5]+bv[10][5]+bv[11][5]+bv[12][5]+bv[13][5]+bv[14][5]+bv[15][5]+bv[16][5]+bv[17][5]+bv[18][5]+bv[19][5]+bv[20][5]+bv[21][5]+bv[22][5]+bv[23][5]+bv[24][5]+bv[25][5] == 8,
bv[1][6]+bv[2][6]+bv[3][6]+bv[4][6]+bv[5][6]+bv[6][6]+bv[7][6]+bv[8][6]+bv[9][6]+bv[10][6]+bv[11][6]+bv[12][6]+bv[13][6]+bv[14][6]+bv[15][6]+bv[16][6]+bv[17][6]+bv[18][6]+bv[19][6]+bv[20][6]+bv[21][6]+bv[22][6]+bv[23][6]+bv[24][6]+bv[25][6] == 10,
bv[1][7]+bv[2][7]+bv[3][7]+bv[4][7]+bv[5][7]+bv[6][7]+bv[7][7]+bv[8][7]+bv[9][7]+bv[10][7]+bv[11][7]+bv[12][7]+bv[13][7]+bv[14][7]+bv[15][7]+bv[16][7]+bv[17][7]+bv[18][7]+bv[19][7]+bv[20][7]+bv[21][7]+bv[22][7]+bv[23][7]+bv[24][7]+bv[25][7] == 4,
bv[1][8]+bv[2][8]+bv[3][8]+bv[4][8]+bv[5][8]+bv[6][8]+bv[7][8]+bv[8][8]+bv[9][8]+bv[10][8]+bv[11][8]+bv[12][8]+bv[13][8]+bv[14][8]+bv[15][8]+bv[16][8]+bv[17][8]+bv[18][8]+bv[19][8]+bv[20][8]+bv[21][8]+bv[22][8]+bv[23][8]+bv[24][8]+bv[25][8] == 6,
bv[1][9]+bv[2][9]+bv[3][9]+bv[4][9]+bv[5][9]+bv[6][9]+bv[7][9]+bv[8][9]+bv[9][9]+bv[10][9]+bv[11][9]+bv[12][9]+bv[13][9]+bv[14][9]+bv[15][9]+bv[16][9]+bv[17][9]+bv[18][9]+bv[19][9]+bv[20][9]+bv[21][9]+bv[22][9]+bv[23][9]+bv[24][9]+bv[25][9] == 9,
bv[1][10]+bv[2][10]+bv[3][10]+bv[4][10]+bv[5][10]+bv[6][10]+bv[7][10]+bv[8][10]+bv[9][10]+bv[10][10]+bv[11][10]+bv[12][10]+bv[13][10]+bv[14][10]+bv[15][10]+bv[16][10]+bv[17][10]+bv[18][10]+bv[19][10]+bv[20][10]+bv[21][10]+bv[22][10]+bv[23][10]+bv[24][10]+bv[25][10] == 7,
bv[1][11]+bv[2][11]+bv[3][11]+bv[4][11]+bv[5][11]+bv[6][11]+bv[7][11]+bv[8][11]+bv[9][11]+bv[10][11]+bv[11][11]+bv[12][11]+bv[13][11]+bv[14][11]+bv[15][11]+bv[16][11]+bv[17][11]+bv[18][11]+bv[19][11]+bv[20][11]+bv[21][11]+bv[22][11]+bv[23][11]+bv[24][11]+bv[25][11] == 5,
bv[1][12]+bv[2][12]+bv[3][12]+bv[4][12]+bv[5][12]+bv[6][12]+bv[7][12]+bv[8][12]+bv[9][12]+bv[10][12]+bv[11][12]+bv[12][12]+bv[13][12]+bv[14][12]+bv[15][12]+bv[16][12]+bv[17][12]+bv[18][12]+bv[19][12]+bv[20][12]+bv[21][12]+bv[22][12]+bv[23][12]+bv[24][12]+bv[25][12] == 7,
bv[1][13]+bv[2][13]+bv[3][13]+bv[4][13]+bv[5][13]+bv[6][13]+bv[7][13]+bv[8][13]+bv[9][13]+bv[10][13]+bv[11][13]+bv[12][13]+bv[13][13]+bv[14][13]+bv[15][13]+bv[16][13]+bv[17][13]+bv[18][13]+bv[19][13]+bv[20][13]+bv[21][13]+bv[22][13]+bv[23][13]+bv[24][13]+bv[25][13] == 6,
bv[1][14]+bv[2][14]+bv[3][14]+bv[4][14]+bv[5][14]+bv[6][14]+bv[7][14]+bv[8][14]+bv[9][14]+bv[10][14]+bv[11][14]+bv[12][14]+bv[13][14]+bv[14][14]+bv[15][14]+bv[16][14]+bv[17][14]+bv[18][14]+bv[19][14]+bv[20][14]+bv[21][14]+bv[22][14]+bv[23][14]+bv[24][14]+bv[25][14] == 8,
bv[1][15]+bv[2][15]+bv[3][15]+bv[4][15]+bv[5][15]+bv[6][15]+bv[7][15]+bv[8][15]+bv[9][15]+bv[10][15]+bv[11][15]+bv[12][15]+bv[13][15]+bv[14][15]+bv[15][15]+bv[16][15]+bv[17][15]+bv[18][15]+bv[19][15]+bv[20][15]+bv[21][15]+bv[22][15]+bv[23][15]+bv[24][15]+bv[25][15] == 5,
bv[1][16]+bv[2][16]+bv[3][16]+bv[4][16]+bv[5][16]+bv[6][16]+bv[7][16]+bv[8][16]+bv[9][16]+bv[10][16]+bv[11][16]+bv[12][16]+bv[13][16]+bv[14][16]+bv[15][16]+bv[16][16]+bv[17][16]+bv[18][16]+bv[19][16]+bv[20][16]+bv[21][16]+bv[22][16]+bv[23][16]+bv[24][16]+bv[25][16] == 7,
bv[1][17]+bv[2][17]+bv[3][17]+bv[4][17]+bv[5][17]+bv[6][17]+bv[7][17]+bv[8][17]+bv[9][17]+bv[10][17]+bv[11][17]+bv[12][17]+bv[13][17]+bv[14][17]+bv[15][17]+bv[16][17]+bv[17][17]+bv[18][17]+bv[19][17]+bv[20][17]+bv[21][17]+bv[22][17]+bv[23][17]+bv[24][17]+bv[25][17] == 4,
bv[1][18]+bv[2][18]+bv[3][18]+bv[4][18]+bv[5][18]+bv[6][18]+bv[7][18]+bv[8][18]+bv[9][18]+bv[10][18]+bv[11][18]+bv[12][18]+bv[13][18]+bv[14][18]+bv[15][18]+bv[16][18]+bv[17][18]+bv[18][18]+bv[19][18]+bv[20][18]+bv[21][18]+bv[22][18]+bv[23][18]+bv[24][18]+bv[25][18] == 6,
bv[1][19]+bv[2][19]+bv[3][19]+bv[4][19]+bv[5][19]+bv[6][19]+bv[7][19]+bv[8][19]+bv[9][19]+bv[10][19]+bv[11][19]+bv[12][19]+bv[13][19]+bv[14][19]+bv[15][19]+bv[16][19]+bv[17][19]+bv[18][19]+bv[19][19]+bv[20][19]+bv[21][19]+bv[22][19]+bv[23][19]+bv[24][19]+bv[25][19] == 7,
bv[1][20]+bv[2][20]+bv[3][20]+bv[4][20]+bv[5][20]+bv[6][20]+bv[7][20]+bv[8][20]+bv[9][20]+bv[10][20]+bv[11][20]+bv[12][20]+bv[13][20]+bv[14][20]+bv[15][20]+bv[16][20]+bv[17][20]+bv[18][20]+bv[19][20]+bv[20][20]+bv[21][20]+bv[22][20]+bv[23][20]+bv[24][20]+bv[25][20] == 6,
bv[1][21]+bv[2][21]+bv[3][21]+bv[4][21]+bv[5][21]+bv[6][21]+bv[7][21]+bv[8][21]+bv[9][21]+bv[10][21]+bv[11][21]+bv[12][21]+bv[13][21]+bv[14][21]+bv[15][21]+bv[16][21]+bv[17][21]+bv[18][21]+bv[19][21]+bv[20][21]+bv[21][21]+bv[22][21]+bv[23][21]+bv[24][21]+bv[25][21] == 6,
bv[1][22]+bv[2][22]+bv[3][22]+bv[4][22]+bv[5][22]+bv[6][22]+bv[7][22]+bv[8][22]+bv[9][22]+bv[10][22]+bv[11][22]+bv[12][22]+bv[13][22]+bv[14][22]+bv[15][22]+bv[16][22]+bv[17][22]+bv[18][22]+bv[19][22]+bv[20][22]+bv[21][22]+bv[22][22]+bv[23][22]+bv[24][22]+bv[25][22] == 11,
bv[1][23]+bv[2][23]+bv[3][23]+bv[4][23]+bv[5][23]+bv[6][23]+bv[7][23]+bv[8][23]+bv[9][23]+bv[10][23]+bv[11][23]+bv[12][23]+bv[13][23]+bv[14][23]+bv[15][23]+bv[16][23]+bv[17][23]+bv[18][23]+bv[19][23]+bv[20][23]+bv[21][23]+bv[22][23]+bv[23][23]+bv[24][23]+bv[25][23] == 5,
bv[1][24]+bv[2][24]+bv[3][24]+bv[4][24]+bv[5][24]+bv[6][24]+bv[7][24]+bv[8][24]+bv[9][24]+bv[10][24]+bv[11][24]+bv[12][24]+bv[13][24]+bv[14][24]+bv[15][24]+bv[16][24]+bv[17][24]+bv[18][24]+bv[19][24]+bv[20][24]+bv[21][24]+bv[22][24]+bv[23][24]+bv[24][24]+bv[25][24] == 7,
bv[1][25]+bv[2][25]+bv[3][25]+bv[4][25]+bv[5][25]+bv[6][25]+bv[7][25]+bv[8][25]+bv[9][25]+bv[10][25]+bv[11][25]+bv[12][25]+bv[13][25]+bv[14][25]+bv[15][25]+bv[16][25]+bv[17][25]+bv[18][25]+bv[19][25]+bv[20][25]+bv[21][25]+bv[22][25]+bv[23][25]+bv[24][25]+bv[25][25] == 6,
bv[1][26]+bv[2][26]+bv[3][26]+bv[4][26]+bv[5][26]+bv[6][26]+bv[7][26]+bv[8][26]+bv[9][26]+bv[10][26]+bv[11][26]+bv[12][26]+bv[13][26]+bv[14][26]+bv[15][26]+bv[16][26]+bv[17][26]+bv[18][26]+bv[19][26]+bv[20][26]+bv[21][26]+bv[22][26]+bv[23][26]+bv[24][26]+bv[25][26] == 8,
bv[1][27]+bv[2][27]+bv[3][27]+bv[4][27]+bv[5][27]+bv[6][27]+bv[7][27]+bv[8][27]+bv[9][27]+bv[10][27]+bv[11][27]+bv[12][27]+bv[13][27]+bv[14][27]+bv[15][27]+bv[16][27]+bv[17][27]+bv[18][27]+bv[19][27]+bv[20][27]+bv[21][27]+bv[22][27]+bv[23][27]+bv[24][27]+bv[25][27] == 7,
bv[1][28]+bv[2][28]+bv[3][28]+bv[4][28]+bv[5][28]+bv[6][28]+bv[7][28]+bv[8][28]+bv[9][28]+bv[10][28]+bv[11][28]+bv[12][28]+bv[13][28]+bv[14][28]+bv[15][28]+bv[16][28]+bv[17][28]+bv[18][28]+bv[19][28]+bv[20][28]+bv[21][28]+bv[22][28]+bv[23][28]+bv[24][28]+bv[25][28] == 7,
bv[1][29]+bv[2][29]+bv[3][29]+bv[4][29]+bv[5][29]+bv[6][29]+bv[7][29]+bv[8][29]+bv[9][29]+bv[10][29]+bv[11][29]+bv[12][29]+bv[13][29]+bv[14][29]+bv[15][29]+bv[16][29]+bv[17][29]+bv[18][29]+bv[19][29]+bv[20][29]+bv[21][29]+bv[22][29]+bv[23][29]+bv[24][29]+bv[25][29] == 2,
bv[1][30]+bv[2][30]+bv[3][30]+bv[4][30]+bv[5][30]+bv[6][30]+bv[7][30]+bv[8][30]+bv[9][30]+bv[10][30]+bv[11][30]+bv[12][30]+bv[13][30]+bv[14][30]+bv[15][30]+bv[16][30]+bv[17][30]+bv[18][30]+bv[19][30]+bv[20][30]+bv[21][30]+bv[22][30]+bv[23][30]+bv[24][30]+bv[25][30] == 2,
bv[1][1] == 0,
bv[1][2]+bv[2][1] == 0,
bv[1][3]+bv[2][2]+bv[3][1] == 0,
bv[1][4]+bv[2][3]+bv[3][2]+bv[4][1] == 0,
bv[1][5]+bv[2][4]+bv[3][3]+bv[4][2]+bv[5][1] == 0,
bv[1][6]+bv[2][5]+bv[3][4]+bv[4][3]+bv[5][2]+bv[6][1] == 1,
bv[1][7]+bv[2][6]+bv[3][5]+bv[4][4]+bv[5][3]+bv[6][2]+bv[7][1] == 3,
bv[1][8]+bv[2][7]+bv[3][6]+bv[4][5]+bv[5][4]+bv[6][3]+bv[7][2]+bv[8][1] == 2,
bv[1][9]+bv[2][8]+bv[3][7]+bv[4][6]+bv[5][5]+bv[6][4]+bv[7][3]+bv[8][2]+bv[9][1] == 2,
bv[1][10]+bv[2][9]+bv[3][8]+bv[4][7]+bv[5][6]+bv[6][5]+bv[7][4]+bv[8][3]+bv[9][2]+bv[10][1] == 3,
bv[1][11]+bv[2][10]+bv[3][9]+bv[4][8]+bv[5][7]+bv[6][6]+bv[7][5]+bv[8][4]+bv[9][3]+bv[10][2]+bv[11][1] == 3,
bv[1][12]+bv[2][11]+bv[3][10]+bv[4][9]+bv[5][8]+bv[6][7]+bv[7][6]+bv[8][5]+bv[9][4]+bv[10][3]+bv[11][2]+bv[12][1] == 3,
bv[1][13]+bv[2][12]+bv[3][11]+bv[4][10]+bv[5][9]+bv[6][8]+bv[7][7]+bv[8][6]+bv[9][5]+bv[10][4]+bv[11][3]+bv[12][2]+bv[13][1] == 1,
bv[1][14]+bv[2][13]+bv[3][12]+bv[4][11]+bv[5][10]+bv[6][9]+bv[7][8]+bv[8][7]+bv[9][6]+bv[10][5]+bv[11][4]+bv[12][3]+bv[13][2]+bv[14][1] == 4,
bv[1][15]+bv[2][14]+bv[3][13]+bv[4][12]+bv[5][11]+bv[6][10]+bv[7][9]+bv[8][8]+bv[9][7]+bv[10][6]+bv[11][5]+bv[12][4]+bv[13][3]+bv[14][2]+bv[15][1] == 3,
bv[1][16]+bv[2][15]+bv[3][14]+bv[4][13]+bv[5][12]+bv[6][11]+bv[7][10]+bv[8][9]+bv[9][8]+bv[10][7]+bv[11][6]+bv[12][5]+bv[13][4]+bv[14][3]+bv[15][2]+bv[16][1] == 3,
bv[1][17]+bv[2][16]+bv[3][15]+bv[4][14]+bv[5][13]+bv[6][12]+bv[7][11]+bv[8][10]+bv[9][9]+bv[10][8]+bv[11][7]+bv[12][6]+bv[13][5]+bv[14][4]+bv[15][3]+bv[16][2]+bv[17][1] == 4,
bv[1][18]+bv[2][17]+bv[3][16]+bv[4][15]+bv[5][14]+bv[6][13]+bv[7][12]+bv[8][11]+bv[9][10]+bv[10][9]+bv[11][8]+bv[12][7]+bv[13][6]+bv[14][5]+bv[15][4]+bv[16][3]+bv[17][2]+bv[18][1] == 5,
bv[1][19]+bv[2][18]+bv[3][17]+bv[4][16]+bv[5][15]+bv[6][14]+bv[7][13]+bv[8][12]+bv[9][11]+bv[10][10]+bv[11][9]+bv[12][8]+bv[13][7]+bv[14][6]+bv[15][5]+bv[16][4]+bv[17][3]+bv[18][2]+bv[19][1] == 3,
bv[1][20]+bv[2][19]+bv[3][18]+bv[4][17]+bv[5][16]+bv[6][15]+bv[7][14]+bv[8][13]+bv[9][12]+bv[10][11]+bv[11][10]+bv[12][9]+bv[13][8]+bv[14][7]+bv[15][6]+bv[16][5]+bv[17][4]+bv[18][3]+bv[19][2]+bv[20][1] == 5,
bv[1][21]+bv[2][20]+bv[3][19]+bv[4][18]+bv[5][17]+bv[6][16]+bv[7][15]+bv[8][14]+bv[9][13]+bv[10][12]+bv[11][11]+bv[12][10]+bv[13][9]+bv[14][8]+bv[15][7]+bv[16][6]+bv[17][5]+bv[18][4]+bv[19][3]+bv[20][2]+bv[21][1] == 5,
bv[1][22]+bv[2][21]+bv[3][20]+bv[4][19]+bv[5][18]+bv[6][17]+bv[7][16]+bv[8][15]+bv[9][14]+bv[10][13]+bv[11][12]+bv[12][11]+bv[13][10]+bv[14][9]+bv[15][8]+bv[16][7]+bv[17][6]+bv[18][5]+bv[19][4]+bv[20][3]+bv[21][2]+bv[22][1] == 6,
bv[1][23]+bv[2][22]+bv[3][21]+bv[4][20]+bv[5][19]+bv[6][18]+bv[7][17]+bv[8][16]+bv[9][15]+bv[10][14]+bv[11][13]+bv[12][12]+bv[13][11]+bv[14][10]+bv[15][9]+bv[16][8]+bv[17][7]+bv[18][6]+bv[19][5]+bv[20][4]+bv[21][3]+bv[22][2]+bv[23][1] == 3,
bv[1][24]+bv[2][23]+bv[3][22]+bv[4][21]+bv[5][20]+bv[6][19]+bv[7][18]+bv[8][17]+bv[9][16]+bv[10][15]+bv[11][14]+bv[12][13]+bv[13][12]+bv[14][11]+bv[15][10]+bv[16][9]+bv[17][8]+bv[18][7]+bv[19][6]+bv[20][5]+bv[21][4]+bv[22][3]+bv[23][2]+bv[24][1] == 8,
bv[1][25]+bv[2][24]+bv[3][23]+bv[4][22]+bv[5][21]+bv[6][20]+bv[7][19]+bv[8][18]+bv[9][17]+bv[10][16]+bv[11][15]+bv[12][14]+bv[13][13]+bv[14][12]+bv[15][11]+bv[16][10]+bv[17][9]+bv[18][8]+bv[19][7]+bv[20][6]+bv[21][5]+bv[22][4]+bv[23][3]+bv[24][2]+bv[25][1] == 5,
bv[1][26]+bv[2][25]+bv[3][24]+bv[4][23]+bv[5][22]+bv[6][21]+bv[7][20]+bv[8][19]+bv[9][18]+bv[10][17]+bv[11][16]+bv[12][15]+bv[13][14]+bv[14][13]+bv[15][12]+bv[16][11]+bv[17][10]+bv[18][9]+bv[19][8]+bv[20][7]+bv[21][6]+bv[22][5]+bv[23][4]+bv[24][3]+bv[25][2] == 3,
bv[1][27]+bv[2][26]+bv[3][25]+bv[4][24]+bv[5][23]+bv[6][22]+bv[7][21]+bv[8][20]+bv[9][19]+bv[10][18]+bv[11][17]+bv[12][16]+bv[13][15]+bv[14][14]+bv[15][13]+bv[16][12]+bv[17][11]+bv[18][10]+bv[19][9]+bv[20][8]+bv[21][7]+bv[22][6]+bv[23][5]+bv[24][4]+bv[25][3] == 2,
bv[1][28]+bv[2][27]+bv[3][26]+bv[4][25]+bv[5][24]+bv[6][23]+bv[7][22]+bv[8][21]+bv[9][20]+bv[10][19]+bv[11][18]+bv[12][17]+bv[13][16]+bv[14][15]+bv[15][14]+bv[16][13]+bv[17][12]+bv[18][11]+bv[19][10]+bv[20][9]+bv[21][8]+bv[22][7]+bv[23][6]+bv[24][5]+bv[25][4] == 4,
bv[1][29]+bv[2][28]+bv[3][27]+bv[4][26]+bv[5][25]+bv[6][24]+bv[7][23]+bv[8][22]+bv[9][21]+bv[10][20]+bv[11][19]+bv[12][18]+bv[13][17]+bv[14][16]+bv[15][15]+bv[16][14]+bv[17][13]+bv[18][12]+bv[19][11]+bv[20][10]+bv[21][9]+bv[22][8]+bv[23][7]+bv[24][6]+bv[25][5] == 5,
bv[1][30]+bv[2][29]+bv[3][28]+bv[4][27]+bv[5][26]+bv[6][25]+bv[7][24]+bv[8][23]+bv[9][22]+bv[10][21]+bv[11][20]+bv[12][19]+bv[13][18]+bv[14][17]+bv[15][16]+bv[16][15]+bv[17][14]+bv[18][13]+bv[19][12]+bv[20][11]+bv[21][10]+bv[22][9]+bv[23][8]+bv[24][7]+bv[25][6] == 7,
bv[2][30]+bv[3][29]+bv[4][28]+bv[5][27]+bv[6][26]+bv[7][25]+bv[8][24]+bv[9][23]+bv[10][22]+bv[11][21]+bv[12][20]+bv[13][19]+bv[14][18]+bv[15][17]+bv[16][16]+bv[17][15]+bv[18][14]+bv[19][13]+bv[20][12]+bv[21][11]+bv[22][10]+bv[23][9]+bv[24][8]+bv[25][7] == 7,
bv[3][30]+bv[4][29]+bv[5][28]+bv[6][27]+bv[7][26]+bv[8][25]+bv[9][24]+bv[10][23]+bv[11][22]+bv[12][21]+bv[13][20]+bv[14][19]+bv[15][18]+bv[16][17]+bv[17][16]+bv[18][15]+bv[19][14]+bv[20][13]+bv[21][12]+bv[22][11]+bv[23][10]+bv[24][9]+bv[25][8] == 7,
bv[4][30]+bv[5][29]+bv[6][28]+bv[7][27]+bv[8][26]+bv[9][25]+bv[10][24]+bv[11][23]+bv[12][22]+bv[13][21]+bv[14][20]+bv[15][19]+bv[16][18]+bv[17][17]+bv[18][16]+bv[19][15]+bv[20][14]+bv[21][13]+bv[22][12]+bv[23][11]+bv[24][10]+bv[25][9] == 7,
bv[5][30]+bv[6][29]+bv[7][28]+bv[8][27]+bv[9][26]+bv[10][25]+bv[11][24]+bv[12][23]+bv[13][22]+bv[14][21]+bv[15][20]+bv[16][19]+bv[17][18]+bv[18][17]+bv[19][16]+bv[20][15]+bv[21][14]+bv[22][13]+bv[23][12]+bv[24][11]+bv[25][10] == 7,
bv[6][30]+bv[7][29]+bv[8][28]+bv[9][27]+bv[10][26]+bv[11][25]+bv[12][24]+bv[13][23]+bv[14][22]+bv[15][21]+bv[16][20]+bv[17][19]+bv[18][18]+bv[19][17]+bv[20][16]+bv[21][15]+bv[22][14]+bv[23][13]+bv[24][12]+bv[25][11] == 4,
bv[7][30]+bv[8][29]+bv[9][28]+bv[10][27]+bv[11][26]+bv[12][25]+bv[13][24]+bv[14][23]+bv[15][22]+bv[16][21]+bv[17][20]+bv[18][19]+bv[19][18]+bv[20][17]+bv[21][16]+bv[22][15]+bv[23][14]+bv[24][13]+bv[25][12] == 4,
bv[8][30]+bv[9][29]+bv[10][28]+bv[11][27]+bv[12][26]+bv[13][25]+bv[14][24]+bv[15][23]+bv[16][22]+bv[17][21]+bv[18][20]+bv[19][19]+bv[20][18]+bv[21][17]+bv[22][16]+bv[23][15]+bv[24][14]+bv[25][13] == 4,
bv[9][30]+bv[10][29]+bv[11][28]+bv[12][27]+bv[13][26]+bv[14][25]+bv[15][24]+bv[16][23]+bv[17][22]+bv[18][21]+bv[19][20]+bv[20][19]+bv[21][18]+bv[22][17]+bv[23][16]+bv[24][15]+bv[25][14] == 4,
bv[10][30]+bv[11][29]+bv[12][28]+bv[13][27]+bv[14][26]+bv[15][25]+bv[16][24]+bv[17][23]+bv[18][22]+bv[19][21]+bv[20][20]+bv[21][19]+bv[22][18]+bv[23][17]+bv[24][16]+bv[25][15] == 4,
bv[11][30]+bv[12][29]+bv[13][28]+bv[14][27]+bv[15][26]+bv[16][25]+bv[17][24]+bv[18][23]+bv[19][22]+bv[20][21]+bv[21][20]+bv[22][19]+bv[23][18]+bv[24][17]+bv[25][16] == 4,
bv[12][30]+bv[13][29]+bv[14][28]+bv[15][27]+bv[16][26]+bv[17][25]+bv[18][24]+bv[19][23]+bv[20][22]+bv[21][21]+bv[22][20]+bv[23][19]+bv[24][18]+bv[25][17] == 6,
bv[13][30]+bv[14][29]+bv[15][28]+bv[16][27]+bv[17][26]+bv[18][25]+bv[19][24]+bv[20][23]+bv[21][22]+bv[22][21]+bv[23][20]+bv[24][19]+bv[25][18] == 5,
bv[14][30]+bv[15][29]+bv[16][28]+bv[17][27]+bv[18][26]+bv[19][25]+bv[20][24]+bv[21][23]+bv[22][22]+bv[23][21]+bv[24][20]+bv[25][19] == 6,
bv[15][30]+bv[16][29]+bv[17][28]+bv[18][27]+bv[19][26]+bv[20][25]+bv[21][24]+bv[22][23]+bv[23][22]+bv[24][21]+bv[25][20] == 4,
bv[16][30]+bv[17][29]+bv[18][28]+bv[19][27]+bv[20][26]+bv[21][25]+bv[22][24]+bv[23][23]+bv[24][22]+bv[25][21] == 5,
bv[17][30]+bv[18][29]+bv[19][28]+bv[20][27]+bv[21][26]+bv[22][25]+bv[23][24]+bv[24][23]+bv[25][22] == 5,
bv[18][30]+bv[19][29]+bv[20][28]+bv[21][27]+bv[22][26]+bv[23][25]+bv[24][24]+bv[25][23] == 4,
bv[19][30]+bv[20][29]+bv[21][28]+bv[22][27]+bv[23][26]+bv[24][25]+bv[25][24] == 1,
bv[20][30]+bv[21][29]+bv[22][28]+bv[23][27]+bv[24][26]+bv[25][25] == 1,
bv[21][30]+bv[22][29]+bv[23][28]+bv[24][27]+bv[25][26] == 0,
bv[22][30]+bv[23][29]+bv[24][28]+bv[25][27] == 0,
bv[23][30]+bv[24][29]+bv[25][28] == 0,
bv[24][30]+bv[25][29] == 0,
bv[25][30] == 0,
bv[1][30] == 0,
bv[1][29]+bv[2][30] == 0,
bv[1][28]+bv[2][29]+bv[3][30] == 0,
bv[1][27]+bv[2][28]+bv[3][29]+bv[4][30] == 0,
bv[1][26]+bv[2][27]+bv[3][28]+bv[4][29]+bv[5][30] == 0,
bv[1][25]+bv[2][26]+bv[3][27]+bv[4][28]+bv[5][29]+bv[6][30] == 0,
bv[1][24]+bv[2][25]+bv[3][26]+bv[4][27]+bv[5][28]+bv[6][29]+bv[7][30] == 1,
bv[1][23]+bv[2][24]+bv[3][25]+bv[4][26]+bv[5][27]+bv[6][28]+bv[7][29]+bv[8][30] == 2,
bv[1][22]+bv[2][23]+bv[3][24]+bv[4][25]+bv[5][26]+bv[6][27]+bv[7][28]+bv[8][29]+bv[9][30] == 3,
bv[1][21]+bv[2][22]+bv[3][23]+bv[4][24]+bv[5][25]+bv[6][26]+bv[7][27]+bv[8][28]+bv[9][29]+bv[10][30] == 1,
bv[1][20]+bv[2][21]+bv[3][22]+bv[4][23]+bv[5][24]+bv[6][25]+bv[7][26]+bv[8][27]+bv[9][28]+bv[10][29]+bv[11][30] == 2,
bv[1][19]+bv[2][20]+bv[3][21]+bv[4][22]+bv[5][23]+bv[6][24]+bv[7][25]+bv[8][26]+bv[9][27]+bv[10][28]+bv[11][29]+bv[12][30] == 3,
bv[1][18]+bv[2][19]+bv[3][20]+bv[4][21]+bv[5][22]+bv[6][23]+bv[7][24]+bv[8][25]+bv[9][26]+bv[10][27]+bv[11][28]+bv[12][29]+bv[13][30] == 4,
bv[1][17]+bv[2][18]+bv[3][19]+bv[4][20]+bv[5][21]+bv[6][22]+bv[7][23]+bv[8][24]+bv[9][25]+bv[10][26]+bv[11][27]+bv[12][28]+bv[13][29]+bv[14][30] == 3,
bv[1][16]+bv[2][17]+bv[3][18]+bv[4][19]+bv[5][20]+bv[6][21]+bv[7][22]+bv[8][23]+bv[9][24]+bv[10][25]+bv[11][26]+bv[12][27]+bv[13][28]+bv[14][29]+bv[15][30] == 5,
bv[1][15]+bv[2][16]+bv[3][17]+bv[4][18]+bv[5][19]+bv[6][20]+bv[7][21]+bv[8][22]+bv[9][23]+bv[10][24]+bv[11][25]+bv[12][26]+bv[13][27]+bv[14][28]+bv[15][29]+bv[16][30] == 5,
bv[1][14]+bv[2][15]+bv[3][16]+bv[4][17]+bv[5][18]+bv[6][19]+bv[7][20]+bv[8][21]+bv[9][22]+bv[10][23]+bv[11][24]+bv[12][25]+bv[13][26]+bv[14][27]+bv[15][28]+bv[16][29]+bv[17][30] == 3,
bv[1][13]+bv[2][14]+bv[3][15]+bv[4][16]+bv[5][17]+bv[6][18]+bv[7][19]+bv[8][20]+bv[9][21]+bv[10][22]+bv[11][23]+bv[12][24]+bv[13][25]+bv[14][26]+bv[15][27]+bv[16][28]+bv[17][29]+bv[18][30] == 3,
bv[1][12]+bv[2][13]+bv[3][14]+bv[4][15]+bv[5][16]+bv[6][17]+bv[7][18]+bv[8][19]+bv[9][20]+bv[10][21]+bv[11][22]+bv[12][23]+bv[13][24]+bv[14][25]+bv[15][26]+bv[16][27]+bv[17][28]+bv[18][29]+bv[19][30] == 2,
bv[1][11]+bv[2][12]+bv[3][13]+bv[4][14]+bv[5][15]+bv[6][16]+bv[7][17]+bv[8][18]+bv[9][19]+bv[10][20]+bv[11][21]+bv[12][22]+bv[13][23]+bv[14][24]+bv[15][25]+bv[16][26]+bv[17][27]+bv[18][28]+bv[19][29]+bv[20][30] == 4,
bv[1][10]+bv[2][11]+bv[3][12]+bv[4][13]+bv[5][14]+bv[6][15]+bv[7][16]+bv[8][17]+bv[9][18]+bv[10][19]+bv[11][20]+bv[12][21]+bv[13][22]+bv[14][23]+bv[15][24]+bv[16][25]+bv[17][26]+bv[18][27]+bv[19][28]+bv[20][29]+bv[21][30] == 5,
bv[1][9]+bv[2][10]+bv[3][11]+bv[4][12]+bv[5][13]+bv[6][14]+bv[7][15]+bv[8][16]+bv[9][17]+bv[10][18]+bv[11][19]+bv[12][20]+bv[13][21]+bv[14][22]+bv[15][23]+bv[16][24]+bv[17][25]+bv[18][26]+bv[19][27]+bv[20][28]+bv[21][29]+bv[22][30] == 4,
bv[1][8]+bv[2][9]+bv[3][10]+bv[4][11]+bv[5][12]+bv[6][13]+bv[7][14]+bv[8][15]+bv[9][16]+bv[10][17]+bv[11][18]+bv[12][19]+bv[13][20]+bv[14][21]+bv[15][22]+bv[16][23]+bv[17][24]+bv[18][25]+bv[19][26]+bv[20][27]+bv[21][28]+bv[22][29]+bv[23][30] == 4,
bv[1][7]+bv[2][8]+bv[3][9]+bv[4][10]+bv[5][11]+bv[6][12]+bv[7][13]+bv[8][14]+bv[9][15]+bv[10][16]+bv[11][17]+bv[12][18]+bv[13][19]+bv[14][20]+bv[15][21]+bv[16][22]+bv[17][23]+bv[18][24]+bv[19][25]+bv[20][26]+bv[21][27]+bv[22][28]+bv[23][29]+bv[24][30] == 6,
bv[1][6]+bv[2][7]+bv[3][8]+bv[4][9]+bv[5][10]+bv[6][11]+bv[7][12]+bv[8][13]+bv[9][14]+bv[10][15]+bv[11][16]+bv[12][17]+bv[13][18]+bv[14][19]+bv[15][20]+bv[16][21]+bv[17][22]+bv[18][23]+bv[19][24]+bv[20][25]+bv[21][26]+bv[22][27]+bv[23][28]+bv[24][29]+bv[25][30] == 9,
bv[1][5]+bv[2][6]+bv[3][7]+bv[4][8]+bv[5][9]+bv[6][10]+bv[7][11]+bv[8][12]+bv[9][13]+bv[10][14]+bv[11][15]+bv[12][16]+bv[13][17]+bv[14][18]+bv[15][19]+bv[16][20]+bv[17][21]+bv[18][22]+bv[19][23]+bv[20][24]+bv[21][25]+bv[22][26]+bv[23][27]+bv[24][28]+bv[25][29] == 8,
bv[1][4]+bv[2][5]+bv[3][6]+bv[4][7]+bv[5][8]+bv[6][9]+bv[7][10]+bv[8][11]+bv[9][12]+bv[10][13]+bv[11][14]+bv[12][15]+bv[13][16]+bv[14][17]+bv[15][18]+bv[16][19]+bv[17][20]+bv[18][21]+bv[19][22]+bv[20][23]+bv[21][24]+bv[22][25]+bv[23][26]+bv[24][27]+bv[25][28] == 3,
bv[1][3]+bv[2][4]+bv[3][5]+bv[4][6]+bv[5][7]+bv[6][8]+bv[7][9]+bv[8][10]+bv[9][11]+bv[10][12]+bv[11][13]+bv[12][14]+bv[13][15]+bv[14][16]+bv[15][17]+bv[16][18]+bv[17][19]+bv[18][20]+bv[19][21]+bv[20][22]+bv[21][23]+bv[22][24]+bv[23][25]+bv[24][26]+bv[25][27] == 4,
bv[1][2]+bv[2][3]+bv[3][4]+bv[4][5]+bv[5][6]+bv[6][7]+bv[7][8]+bv[8][9]+bv[9][10]+bv[10][11]+bv[11][12]+bv[12][13]+bv[13][14]+bv[14][15]+bv[15][16]+bv[16][17]+bv[17][18]+bv[18][19]+bv[19][20]+bv[20][21]+bv[21][22]+bv[22][23]+bv[23][24]+bv[24][25]+bv[25][26] == 2,
bv[1][1]+bv[2][2]+bv[3][3]+bv[4][4]+bv[5][5]+bv[6][6]+bv[7][7]+bv[8][8]+bv[9][9]+bv[10][10]+bv[11][11]+bv[12][12]+bv[13][13]+bv[14][14]+bv[15][15]+bv[16][16]+bv[17][17]+bv[18][18]+bv[19][19]+bv[20][20]+bv[21][21]+bv[22][22]+bv[23][23]+bv[24][24]+bv[25][25] == 4,
bv[2][1]+bv[3][2]+bv[4][3]+bv[5][4]+bv[6][5]+bv[7][6]+bv[8][7]+bv[9][8]+bv[10][9]+bv[11][10]+bv[12][11]+bv[13][12]+bv[14][13]+bv[15][14]+bv[16][15]+bv[17][16]+bv[18][17]+bv[19][18]+bv[20][19]+bv[21][20]+bv[22][21]+bv[23][22]+bv[24][23]+bv[25][24] == 7,
bv[3][1]+bv[4][2]+bv[5][3]+bv[6][4]+bv[7][5]+bv[8][6]+bv[9][7]+bv[10][8]+bv[11][9]+bv[12][10]+bv[13][11]+bv[14][12]+bv[15][13]+bv[16][14]+bv[17][15]+bv[18][16]+bv[19][17]+bv[20][18]+bv[21][19]+bv[22][20]+bv[23][21]+bv[24][22]+bv[25][23] == 7,
bv[4][1]+bv[5][2]+bv[6][3]+bv[7][4]+bv[8][5]+bv[9][6]+bv[10][7]+bv[11][8]+bv[12][9]+bv[13][10]+bv[14][11]+bv[15][12]+bv[16][13]+bv[17][14]+bv[18][15]+bv[19][16]+bv[20][17]+bv[21][18]+bv[22][19]+bv[23][20]+bv[24][21]+bv[25][22] == 6,
bv[5][1]+bv[6][2]+bv[7][3]+bv[8][4]+bv[9][5]+bv[10][6]+bv[11][7]+bv[12][8]+bv[13][9]+bv[14][10]+bv[15][11]+bv[16][12]+bv[17][13]+bv[18][14]+bv[19][15]+bv[20][16]+bv[21][17]+bv[22][18]+bv[23][19]+bv[24][20]+bv[25][21] == 7,
bv[6][1]+bv[7][2]+bv[8][3]+bv[9][4]+bv[10][5]+bv[11][6]+bv[12][7]+bv[13][8]+bv[14][9]+bv[15][10]+bv[16][11]+bv[17][12]+bv[18][13]+bv[19][14]+bv[20][15]+bv[21][16]+bv[22][17]+bv[23][18]+bv[24][19]+bv[25][20] == 11,
bv[7][1]+bv[8][2]+bv[9][3]+bv[10][4]+bv[11][5]+bv[12][6]+bv[13][7]+bv[14][8]+bv[15][9]+bv[16][10]+bv[17][11]+bv[18][12]+bv[19][13]+bv[20][14]+bv[21][15]+bv[22][16]+bv[23][17]+bv[24][18]+bv[25][19] == 6,
bv[8][1]+bv[9][2]+bv[10][3]+bv[11][4]+bv[12][5]+bv[13][6]+bv[14][7]+bv[15][8]+bv[16][9]+bv[17][10]+bv[18][11]+bv[19][12]+bv[20][13]+bv[21][14]+bv[22][15]+bv[23][16]+bv[24][17]+bv[25][18] == 6,
bv[9][1]+bv[10][2]+bv[11][3]+bv[12][4]+bv[13][5]+bv[14][6]+bv[15][7]+bv[16][8]+bv[17][9]+bv[18][10]+bv[19][11]+bv[20][12]+bv[21][13]+bv[22][14]+bv[23][15]+bv[24][16]+bv[25][17] == 4,
bv[10][1]+bv[11][2]+bv[12][3]+bv[13][4]+bv[14][5]+bv[15][6]+bv[16][7]+bv[17][8]+bv[18][9]+bv[19][10]+bv[20][11]+bv[21][12]+bv[22][13]+bv[23][14]+bv[24][15]+bv[25][16] == 5,
bv[11][1]+bv[12][2]+bv[13][3]+bv[14][4]+bv[15][5]+bv[16][6]+bv[17][7]+bv[18][8]+bv[19][9]+bv[20][10]+bv[21][11]+bv[22][12]+bv[23][13]+bv[24][14]+bv[25][15] == 7,
bv[12][1]+bv[13][2]+bv[14][3]+bv[15][4]+bv[16][5]+bv[17][6]+bv[18][7]+bv[19][8]+bv[20][9]+bv[21][10]+bv[22][11]+bv[23][12]+bv[24][13]+bv[25][14] == 6,
bv[13][1]+bv[14][2]+bv[15][3]+bv[16][4]+bv[17][5]+bv[18][6]+bv[19][7]+bv[20][8]+bv[21][9]+bv[22][10]+bv[23][11]+bv[24][12]+bv[25][13] == 4,
bv[14][1]+bv[15][2]+bv[16][3]+bv[17][4]+bv[18][5]+bv[19][6]+bv[20][7]+bv[21][8]+bv[22][9]+bv[23][10]+bv[24][11]+bv[25][12] == 6,
bv[15][1]+bv[16][2]+bv[17][3]+bv[18][4]+bv[19][5]+bv[20][6]+bv[21][7]+bv[22][8]+bv[23][9]+bv[24][10]+bv[25][11] == 4,
bv[16][1]+bv[17][2]+bv[18][3]+bv[19][4]+bv[20][5]+bv[21][6]+bv[22][7]+bv[23][8]+bv[24][9]+bv[25][10] == 5,
bv[17][1]+bv[18][2]+bv[19][3]+bv[20][4]+bv[21][5]+bv[22][6]+bv[23][7]+bv[24][8]+bv[25][9] == 1,
bv[18][1]+bv[19][2]+bv[20][3]+bv[21][4]+bv[22][5]+bv[23][6]+bv[24][7]+bv[25][8] == 0,
bv[19][1]+bv[20][2]+bv[21][3]+bv[22][4]+bv[23][5]+bv[24][6]+bv[25][7] == 0,
bv[20][1]+bv[21][2]+bv[22][3]+bv[23][4]+bv[24][5]+bv[25][6] == 0,
bv[21][1]+bv[22][2]+bv[23][3]+bv[24][4]+bv[25][5] == 0,
bv[22][1]+bv[23][2]+bv[24][3]+bv[25][4] == 0,
bv[23][1]+bv[24][2]+bv[25][3] == 0,
bv[24][1]+bv[25][2] == 0,
bv[25][1] == 0,
]

p = cp.Problem(cp.Minimize(obj), constraints)
result = p.solve()
print(result)

result = p.solve(method="admm", iterations=5, solver="ecos")
print(result)

obj = bv[1][24].z.value[0]+bv[2][5].z.value[0]+bv[2][6].z.value[0]+bv[2][7].z.value[0]+bv[2][23].z.value[0]+bv[2][24].z.value[0]+bv[3][5].z.value[0]+bv[3][7].z.value[0]+bv[3][8].z.value[0]+bv[3][22].z.value[0]+bv[3][25].z.value[0]+bv[4][4].z.value[0]+bv[4][8].z.value[0]+bv[4][9].z.value[0]+bv[4][13].z.value[0]+bv[4][14].z.value[0]+bv[4][15].z.value[0]+bv[4][16].z.value[0]+bv[4][17].z.value[0]+bv[4][18].z.value[0]+bv[4][19].z.value[0]+bv[4][22].z.value[0]+bv[4][25].z.value[0]+bv[5][4].z.value[0]+bv[5][6].z.value[0]+bv[5][9].z.value[0]+bv[5][10].z.value[0]+bv[5][11].z.value[0]+bv[5][12].z.value[0]+bv[5][20].z.value[0]+bv[5][21].z.value[0]+bv[5][22].z.value[0]+bv[5][26].z.value[0]+bv[6][4].z.value[0]+bv[6][6].z.value[0]+bv[6][9].z.value[0]+bv[6][22].z.value[0]+bv[6][24].z.value[0]+bv[6][26].z.value[0]+bv[7][4].z.value[0]+bv[7][6].z.value[0]+bv[7][9].z.value[0]+bv[7][22].z.value[0]+bv[7][24].z.value[0]+bv[7][26].z.value[0]+bv[8][4].z.value[0]+bv[8][22].z.value[0]+bv[8][26].z.value[0]+bv[9][4].z.value[0]+bv[9][23].z.value[0]+bv[9][26].z.value[0]+bv[10][5].z.value[0]+bv[10][25].z.value[0]+bv[10][27].z.value[0]+bv[11][6].z.value[0]+bv[11][27].z.value[0]+bv[12][6].z.value[0]+bv[12][9].z.value[0]+bv[12][10].z.value[0]+bv[12][11].z.value[0]+bv[12][19].z.value[0]+bv[12][20].z.value[0]+bv[12][21].z.value[0]+bv[12][27].z.value[0]+bv[13][6].z.value[0]+bv[13][8].z.value[0]+bv[13][12].z.value[0]+bv[13][18].z.value[0]+bv[13][22].z.value[0]+bv[13][27].z.value[0]+bv[14][1].z.value[0]+bv[14][2].z.value[0]+bv[14][5].z.value[0]+bv[14][8].z.value[0]+bv[14][9].z.value[0]+bv[14][10].z.value[0]+bv[14][12].z.value[0]+bv[14][18].z.value[0]+bv[14][19].z.value[0]+bv[14][20].z.value[0]+bv[14][22].z.value[0]+bv[14][28].z.value[0]+bv[15][3].z.value[0]+bv[15][4].z.value[0]+bv[15][5].z.value[0]+bv[15][8].z.value[0]+bv[15][9].z.value[0]+bv[15][10].z.value[0]+bv[15][11].z.value[0]+bv[15][12].z.value[0]+bv[15][19].z.value[0]+bv[15][20].z.value[0]+bv[15][21].z.value[0]+bv[15][28].z.value[0]+bv[16][5].z.value[0]+bv[16][6].z.value[0]+bv[16][14].z.value[0]+bv[16][16].z.value[0]+bv[16][28].z.value[0]+bv[17][1].z.value[0]+bv[17][2].z.value[0]+bv[17][3].z.value[0]+bv[17][4].z.value[0]+bv[17][14].z.value[0]+bv[17][16].z.value[0]+bv[17][27].z.value[0]+bv[17][28].z.value[0]+bv[17][29].z.value[0]+bv[17][30].z.value[0]+bv[18][4].z.value[0]+bv[18][5].z.value[0]+bv[18][6].z.value[0]+bv[18][7].z.value[0]+bv[18][13].z.value[0]+bv[18][16].z.value[0]+bv[18][23].z.value[0]+bv[18][24].z.value[0]+bv[18][25].z.value[0]+bv[18][26].z.value[0]+bv[18][28].z.value[0]+bv[19][4].z.value[0]+bv[19][14].z.value[0]+bv[19][15].z.value[0]+bv[19][28].z.value[0]+bv[20][5].z.value[0]+bv[20][9].z.value[0]+bv[20][10].z.value[0]+bv[20][22].z.value[0]+bv[20][23].z.value[0]+bv[20][24].z.value[0]+bv[20][25].z.value[0]+bv[20][26].z.value[0]+bv[20][27].z.value[0]+bv[20][28].z.value[0]+bv[20][29].z.value[0]+bv[20][30].z.value[0]+bv[21][6].z.value[0]+bv[21][10].z.value[0]+bv[21][11].z.value[0]+bv[21][12].z.value[0]+bv[21][13].z.value[0]+bv[21][14].z.value[0]+bv[21][27].z.value[0]+bv[22][7].z.value[0]+bv[22][8].z.value[0]+bv[22][12].z.value[0]+bv[22][13].z.value[0]+bv[22][14].z.value[0]+bv[22][15].z.value[0]+bv[22][16].z.value[0]+bv[22][17].z.value[0]+bv[22][18].z.value[0]+bv[22][19].z.value[0]+bv[22][20].z.value[0]+bv[22][21].z.value[0]+bv[22][22].z.value[0]+bv[22][26].z.value[0]+bv[23][9].z.value[0]+bv[23][10].z.value[0]+bv[23][13].z.value[0]+bv[23][14].z.value[0]+bv[23][15].z.value[0]+bv[23][16].z.value[0]+bv[23][17].z.value[0]+bv[23][18].z.value[0]+bv[23][19].z.value[0]+bv[23][24].z.value[0]+bv[23][25].z.value[0]+bv[24][11].z.value[0]+bv[24][21].z.value[0]+bv[24][22].z.value[0]+bv[24][23].z.value[0]+bv[25][12].z.value[0]+bv[25][13].z.value[0]+bv[25][14].z.value[0]+bv[25][15].z.value[0]+bv[25][16].z.value[0]+bv[25][17].z.value[0]+bv[25][18].z.value[0]+bv[25][19].z.value[0]+bv[25][20].z.value[0]+bv[25][21].z.value[0]

constraints = [
bv[1][1].z.value[0]+bv[1][2].z.value[0]+bv[1][3].z.value[0]+bv[1][4].z.value[0]+bv[1][5].z.value[0]+bv[1][6].z.value[0]+bv[1][7].z.value[0]+bv[1][8].z.value[0]+bv[1][9].z.value[0]+bv[1][10].z.value[0]+bv[1][11].z.value[0]+bv[1][12].z.value[0]+bv[1][13].z.value[0]+bv[1][14].z.value[0]+bv[1][15].z.value[0]+bv[1][16].z.value[0]+bv[1][17].z.value[0]+bv[1][18].z.value[0]+bv[1][19].z.value[0]+bv[1][20].z.value[0]+bv[1][21].z.value[0]+bv[1][22].z.value[0]+bv[1][23].z.value[0]+bv[1][24].z.value[0]+bv[1][25].z.value[0]+bv[1][26].z.value[0]+bv[1][27].z.value[0]+bv[1][28].z.value[0]+bv[1][29].z.value[0]+bv[1][30].z.value[0] == 1,
bv[2][1].z.value[0]+bv[2][2].z.value[0]+bv[2][3].z.value[0]+bv[2][4].z.value[0]+bv[2][5].z.value[0]+bv[2][6].z.value[0]+bv[2][7].z.value[0]+bv[2][8].z.value[0]+bv[2][9].z.value[0]+bv[2][10].z.value[0]+bv[2][11].z.value[0]+bv[2][12].z.value[0]+bv[2][13].z.value[0]+bv[2][14].z.value[0]+bv[2][15].z.value[0]+bv[2][16].z.value[0]+bv[2][17].z.value[0]+bv[2][18].z.value[0]+bv[2][19].z.value[0]+bv[2][20].z.value[0]+bv[2][21].z.value[0]+bv[2][22].z.value[0]+bv[2][23].z.value[0]+bv[2][24].z.value[0]+bv[2][25].z.value[0]+bv[2][26].z.value[0]+bv[2][27].z.value[0]+bv[2][28].z.value[0]+bv[2][29].z.value[0]+bv[2][30].z.value[0] == 5,
bv[3][1].z.value[0]+bv[3][2].z.value[0]+bv[3][3].z.value[0]+bv[3][4].z.value[0]+bv[3][5].z.value[0]+bv[3][6].z.value[0]+bv[3][7].z.value[0]+bv[3][8].z.value[0]+bv[3][9].z.value[0]+bv[3][10].z.value[0]+bv[3][11].z.value[0]+bv[3][12].z.value[0]+bv[3][13].z.value[0]+bv[3][14].z.value[0]+bv[3][15].z.value[0]+bv[3][16].z.value[0]+bv[3][17].z.value[0]+bv[3][18].z.value[0]+bv[3][19].z.value[0]+bv[3][20].z.value[0]+bv[3][21].z.value[0]+bv[3][22].z.value[0]+bv[3][23].z.value[0]+bv[3][24].z.value[0]+bv[3][25].z.value[0]+bv[3][26].z.value[0]+bv[3][27].z.value[0]+bv[3][28].z.value[0]+bv[3][29].z.value[0]+bv[3][30].z.value[0] == 5,
bv[4][1].z.value[0]+bv[4][2].z.value[0]+bv[4][3].z.value[0]+bv[4][4].z.value[0]+bv[4][5].z.value[0]+bv[4][6].z.value[0]+bv[4][7].z.value[0]+bv[4][8].z.value[0]+bv[4][9].z.value[0]+bv[4][10].z.value[0]+bv[4][11].z.value[0]+bv[4][12].z.value[0]+bv[4][13].z.value[0]+bv[4][14].z.value[0]+bv[4][15].z.value[0]+bv[4][16].z.value[0]+bv[4][17].z.value[0]+bv[4][18].z.value[0]+bv[4][19].z.value[0]+bv[4][20].z.value[0]+bv[4][21].z.value[0]+bv[4][22].z.value[0]+bv[4][23].z.value[0]+bv[4][24].z.value[0]+bv[4][25].z.value[0]+bv[4][26].z.value[0]+bv[4][27].z.value[0]+bv[4][28].z.value[0]+bv[4][29].z.value[0]+bv[4][30].z.value[0] == 12,
bv[5][1].z.value[0]+bv[5][2].z.value[0]+bv[5][3].z.value[0]+bv[5][4].z.value[0]+bv[5][5].z.value[0]+bv[5][6].z.value[0]+bv[5][7].z.value[0]+bv[5][8].z.value[0]+bv[5][9].z.value[0]+bv[5][10].z.value[0]+bv[5][11].z.value[0]+bv[5][12].z.value[0]+bv[5][13].z.value[0]+bv[5][14].z.value[0]+bv[5][15].z.value[0]+bv[5][16].z.value[0]+bv[5][17].z.value[0]+bv[5][18].z.value[0]+bv[5][19].z.value[0]+bv[5][20].z.value[0]+bv[5][21].z.value[0]+bv[5][22].z.value[0]+bv[5][23].z.value[0]+bv[5][24].z.value[0]+bv[5][25].z.value[0]+bv[5][26].z.value[0]+bv[5][27].z.value[0]+bv[5][28].z.value[0]+bv[5][29].z.value[0]+bv[5][30].z.value[0] == 10,
bv[6][1].z.value[0]+bv[6][2].z.value[0]+bv[6][3].z.value[0]+bv[6][4].z.value[0]+bv[6][5].z.value[0]+bv[6][6].z.value[0]+bv[6][7].z.value[0]+bv[6][8].z.value[0]+bv[6][9].z.value[0]+bv[6][10].z.value[0]+bv[6][11].z.value[0]+bv[6][12].z.value[0]+bv[6][13].z.value[0]+bv[6][14].z.value[0]+bv[6][15].z.value[0]+bv[6][16].z.value[0]+bv[6][17].z.value[0]+bv[6][18].z.value[0]+bv[6][19].z.value[0]+bv[6][20].z.value[0]+bv[6][21].z.value[0]+bv[6][22].z.value[0]+bv[6][23].z.value[0]+bv[6][24].z.value[0]+bv[6][25].z.value[0]+bv[6][26].z.value[0]+bv[6][27].z.value[0]+bv[6][28].z.value[0]+bv[6][29].z.value[0]+bv[6][30].z.value[0] == 6,
bv[7][1].z.value[0]+bv[7][2].z.value[0]+bv[7][3].z.value[0]+bv[7][4].z.value[0]+bv[7][5].z.value[0]+bv[7][6].z.value[0]+bv[7][7].z.value[0]+bv[7][8].z.value[0]+bv[7][9].z.value[0]+bv[7][10].z.value[0]+bv[7][11].z.value[0]+bv[7][12].z.value[0]+bv[7][13].z.value[0]+bv[7][14].z.value[0]+bv[7][15].z.value[0]+bv[7][16].z.value[0]+bv[7][17].z.value[0]+bv[7][18].z.value[0]+bv[7][19].z.value[0]+bv[7][20].z.value[0]+bv[7][21].z.value[0]+bv[7][22].z.value[0]+bv[7][23].z.value[0]+bv[7][24].z.value[0]+bv[7][25].z.value[0]+bv[7][26].z.value[0]+bv[7][27].z.value[0]+bv[7][28].z.value[0]+bv[7][29].z.value[0]+bv[7][30].z.value[0] == 6,
bv[8][1].z.value[0]+bv[8][2].z.value[0]+bv[8][3].z.value[0]+bv[8][4].z.value[0]+bv[8][5].z.value[0]+bv[8][6].z.value[0]+bv[8][7].z.value[0]+bv[8][8].z.value[0]+bv[8][9].z.value[0]+bv[8][10].z.value[0]+bv[8][11].z.value[0]+bv[8][12].z.value[0]+bv[8][13].z.value[0]+bv[8][14].z.value[0]+bv[8][15].z.value[0]+bv[8][16].z.value[0]+bv[8][17].z.value[0]+bv[8][18].z.value[0]+bv[8][19].z.value[0]+bv[8][20].z.value[0]+bv[8][21].z.value[0]+bv[8][22].z.value[0]+bv[8][23].z.value[0]+bv[8][24].z.value[0]+bv[8][25].z.value[0]+bv[8][26].z.value[0]+bv[8][27].z.value[0]+bv[8][28].z.value[0]+bv[8][29].z.value[0]+bv[8][30].z.value[0] == 3,
bv[9][1].z.value[0]+bv[9][2].z.value[0]+bv[9][3].z.value[0]+bv[9][4].z.value[0]+bv[9][5].z.value[0]+bv[9][6].z.value[0]+bv[9][7].z.value[0]+bv[9][8].z.value[0]+bv[9][9].z.value[0]+bv[9][10].z.value[0]+bv[9][11].z.value[0]+bv[9][12].z.value[0]+bv[9][13].z.value[0]+bv[9][14].z.value[0]+bv[9][15].z.value[0]+bv[9][16].z.value[0]+bv[9][17].z.value[0]+bv[9][18].z.value[0]+bv[9][19].z.value[0]+bv[9][20].z.value[0]+bv[9][21].z.value[0]+bv[9][22].z.value[0]+bv[9][23].z.value[0]+bv[9][24].z.value[0]+bv[9][25].z.value[0]+bv[9][26].z.value[0]+bv[9][27].z.value[0]+bv[9][28].z.value[0]+bv[9][29].z.value[0]+bv[9][30].z.value[0] == 3,
bv[10][1].z.value[0]+bv[10][2].z.value[0]+bv[10][3].z.value[0]+bv[10][4].z.value[0]+bv[10][5].z.value[0]+bv[10][6].z.value[0]+bv[10][7].z.value[0]+bv[10][8].z.value[0]+bv[10][9].z.value[0]+bv[10][10].z.value[0]+bv[10][11].z.value[0]+bv[10][12].z.value[0]+bv[10][13].z.value[0]+bv[10][14].z.value[0]+bv[10][15].z.value[0]+bv[10][16].z.value[0]+bv[10][17].z.value[0]+bv[10][18].z.value[0]+bv[10][19].z.value[0]+bv[10][20].z.value[0]+bv[10][21].z.value[0]+bv[10][22].z.value[0]+bv[10][23].z.value[0]+bv[10][24].z.value[0]+bv[10][25].z.value[0]+bv[10][26].z.value[0]+bv[10][27].z.value[0]+bv[10][28].z.value[0]+bv[10][29].z.value[0]+bv[10][30].z.value[0] == 3,
bv[11][1].z.value[0]+bv[11][2].z.value[0]+bv[11][3].z.value[0]+bv[11][4].z.value[0]+bv[11][5].z.value[0]+bv[11][6].z.value[0]+bv[11][7].z.value[0]+bv[11][8].z.value[0]+bv[11][9].z.value[0]+bv[11][10].z.value[0]+bv[11][11].z.value[0]+bv[11][12].z.value[0]+bv[11][13].z.value[0]+bv[11][14].z.value[0]+bv[11][15].z.value[0]+bv[11][16].z.value[0]+bv[11][17].z.value[0]+bv[11][18].z.value[0]+bv[11][19].z.value[0]+bv[11][20].z.value[0]+bv[11][21].z.value[0]+bv[11][22].z.value[0]+bv[11][23].z.value[0]+bv[11][24].z.value[0]+bv[11][25].z.value[0]+bv[11][26].z.value[0]+bv[11][27].z.value[0]+bv[11][28].z.value[0]+bv[11][29].z.value[0]+bv[11][30].z.value[0] == 2,
bv[12][1].z.value[0]+bv[12][2].z.value[0]+bv[12][3].z.value[0]+bv[12][4].z.value[0]+bv[12][5].z.value[0]+bv[12][6].z.value[0]+bv[12][7].z.value[0]+bv[12][8].z.value[0]+bv[12][9].z.value[0]+bv[12][10].z.value[0]+bv[12][11].z.value[0]+bv[12][12].z.value[0]+bv[12][13].z.value[0]+bv[12][14].z.value[0]+bv[12][15].z.value[0]+bv[12][16].z.value[0]+bv[12][17].z.value[0]+bv[12][18].z.value[0]+bv[12][19].z.value[0]+bv[12][20].z.value[0]+bv[12][21].z.value[0]+bv[12][22].z.value[0]+bv[12][23].z.value[0]+bv[12][24].z.value[0]+bv[12][25].z.value[0]+bv[12][26].z.value[0]+bv[12][27].z.value[0]+bv[12][28].z.value[0]+bv[12][29].z.value[0]+bv[12][30].z.value[0] == 8,
bv[13][1].z.value[0]+bv[13][2].z.value[0]+bv[13][3].z.value[0]+bv[13][4].z.value[0]+bv[13][5].z.value[0]+bv[13][6].z.value[0]+bv[13][7].z.value[0]+bv[13][8].z.value[0]+bv[13][9].z.value[0]+bv[13][10].z.value[0]+bv[13][11].z.value[0]+bv[13][12].z.value[0]+bv[13][13].z.value[0]+bv[13][14].z.value[0]+bv[13][15].z.value[0]+bv[13][16].z.value[0]+bv[13][17].z.value[0]+bv[13][18].z.value[0]+bv[13][19].z.value[0]+bv[13][20].z.value[0]+bv[13][21].z.value[0]+bv[13][22].z.value[0]+bv[13][23].z.value[0]+bv[13][24].z.value[0]+bv[13][25].z.value[0]+bv[13][26].z.value[0]+bv[13][27].z.value[0]+bv[13][28].z.value[0]+bv[13][29].z.value[0]+bv[13][30].z.value[0] == 6,
bv[14][1].z.value[0]+bv[14][2].z.value[0]+bv[14][3].z.value[0]+bv[14][4].z.value[0]+bv[14][5].z.value[0]+bv[14][6].z.value[0]+bv[14][7].z.value[0]+bv[14][8].z.value[0]+bv[14][9].z.value[0]+bv[14][10].z.value[0]+bv[14][11].z.value[0]+bv[14][12].z.value[0]+bv[14][13].z.value[0]+bv[14][14].z.value[0]+bv[14][15].z.value[0]+bv[14][16].z.value[0]+bv[14][17].z.value[0]+bv[14][18].z.value[0]+bv[14][19].z.value[0]+bv[14][20].z.value[0]+bv[14][21].z.value[0]+bv[14][22].z.value[0]+bv[14][23].z.value[0]+bv[14][24].z.value[0]+bv[14][25].z.value[0]+bv[14][26].z.value[0]+bv[14][27].z.value[0]+bv[14][28].z.value[0]+bv[14][29].z.value[0]+bv[14][30].z.value[0] == 12,
bv[15][1].z.value[0]+bv[15][2].z.value[0]+bv[15][3].z.value[0]+bv[15][4].z.value[0]+bv[15][5].z.value[0]+bv[15][6].z.value[0]+bv[15][7].z.value[0]+bv[15][8].z.value[0]+bv[15][9].z.value[0]+bv[15][10].z.value[0]+bv[15][11].z.value[0]+bv[15][12].z.value[0]+bv[15][13].z.value[0]+bv[15][14].z.value[0]+bv[15][15].z.value[0]+bv[15][16].z.value[0]+bv[15][17].z.value[0]+bv[15][18].z.value[0]+bv[15][19].z.value[0]+bv[15][20].z.value[0]+bv[15][21].z.value[0]+bv[15][22].z.value[0]+bv[15][23].z.value[0]+bv[15][24].z.value[0]+bv[15][25].z.value[0]+bv[15][26].z.value[0]+bv[15][27].z.value[0]+bv[15][28].z.value[0]+bv[15][29].z.value[0]+bv[15][30].z.value[0] == 12,
bv[16][1].z.value[0]+bv[16][2].z.value[0]+bv[16][3].z.value[0]+bv[16][4].z.value[0]+bv[16][5].z.value[0]+bv[16][6].z.value[0]+bv[16][7].z.value[0]+bv[16][8].z.value[0]+bv[16][9].z.value[0]+bv[16][10].z.value[0]+bv[16][11].z.value[0]+bv[16][12].z.value[0]+bv[16][13].z.value[0]+bv[16][14].z.value[0]+bv[16][15].z.value[0]+bv[16][16].z.value[0]+bv[16][17].z.value[0]+bv[16][18].z.value[0]+bv[16][19].z.value[0]+bv[16][20].z.value[0]+bv[16][21].z.value[0]+bv[16][22].z.value[0]+bv[16][23].z.value[0]+bv[16][24].z.value[0]+bv[16][25].z.value[0]+bv[16][26].z.value[0]+bv[16][27].z.value[0]+bv[16][28].z.value[0]+bv[16][29].z.value[0]+bv[16][30].z.value[0] == 5,
bv[17][1].z.value[0]+bv[17][2].z.value[0]+bv[17][3].z.value[0]+bv[17][4].z.value[0]+bv[17][5].z.value[0]+bv[17][6].z.value[0]+bv[17][7].z.value[0]+bv[17][8].z.value[0]+bv[17][9].z.value[0]+bv[17][10].z.value[0]+bv[17][11].z.value[0]+bv[17][12].z.value[0]+bv[17][13].z.value[0]+bv[17][14].z.value[0]+bv[17][15].z.value[0]+bv[17][16].z.value[0]+bv[17][17].z.value[0]+bv[17][18].z.value[0]+bv[17][19].z.value[0]+bv[17][20].z.value[0]+bv[17][21].z.value[0]+bv[17][22].z.value[0]+bv[17][23].z.value[0]+bv[17][24].z.value[0]+bv[17][25].z.value[0]+bv[17][26].z.value[0]+bv[17][27].z.value[0]+bv[17][28].z.value[0]+bv[17][29].z.value[0]+bv[17][30].z.value[0] == 10,
bv[18][1].z.value[0]+bv[18][2].z.value[0]+bv[18][3].z.value[0]+bv[18][4].z.value[0]+bv[18][5].z.value[0]+bv[18][6].z.value[0]+bv[18][7].z.value[0]+bv[18][8].z.value[0]+bv[18][9].z.value[0]+bv[18][10].z.value[0]+bv[18][11].z.value[0]+bv[18][12].z.value[0]+bv[18][13].z.value[0]+bv[18][14].z.value[0]+bv[18][15].z.value[0]+bv[18][16].z.value[0]+bv[18][17].z.value[0]+bv[18][18].z.value[0]+bv[18][19].z.value[0]+bv[18][20].z.value[0]+bv[18][21].z.value[0]+bv[18][22].z.value[0]+bv[18][23].z.value[0]+bv[18][24].z.value[0]+bv[18][25].z.value[0]+bv[18][26].z.value[0]+bv[18][27].z.value[0]+bv[18][28].z.value[0]+bv[18][29].z.value[0]+bv[18][30].z.value[0] == 11,
bv[19][1].z.value[0]+bv[19][2].z.value[0]+bv[19][3].z.value[0]+bv[19][4].z.value[0]+bv[19][5].z.value[0]+bv[19][6].z.value[0]+bv[19][7].z.value[0]+bv[19][8].z.value[0]+bv[19][9].z.value[0]+bv[19][10].z.value[0]+bv[19][11].z.value[0]+bv[19][12].z.value[0]+bv[19][13].z.value[0]+bv[19][14].z.value[0]+bv[19][15].z.value[0]+bv[19][16].z.value[0]+bv[19][17].z.value[0]+bv[19][18].z.value[0]+bv[19][19].z.value[0]+bv[19][20].z.value[0]+bv[19][21].z.value[0]+bv[19][22].z.value[0]+bv[19][23].z.value[0]+bv[19][24].z.value[0]+bv[19][25].z.value[0]+bv[19][26].z.value[0]+bv[19][27].z.value[0]+bv[19][28].z.value[0]+bv[19][29].z.value[0]+bv[19][30].z.value[0] == 4,
bv[20][1].z.value[0]+bv[20][2].z.value[0]+bv[20][3].z.value[0]+bv[20][4].z.value[0]+bv[20][5].z.value[0]+bv[20][6].z.value[0]+bv[20][7].z.value[0]+bv[20][8].z.value[0]+bv[20][9].z.value[0]+bv[20][10].z.value[0]+bv[20][11].z.value[0]+bv[20][12].z.value[0]+bv[20][13].z.value[0]+bv[20][14].z.value[0]+bv[20][15].z.value[0]+bv[20][16].z.value[0]+bv[20][17].z.value[0]+bv[20][18].z.value[0]+bv[20][19].z.value[0]+bv[20][20].z.value[0]+bv[20][21].z.value[0]+bv[20][22].z.value[0]+bv[20][23].z.value[0]+bv[20][24].z.value[0]+bv[20][25].z.value[0]+bv[20][26].z.value[0]+bv[20][27].z.value[0]+bv[20][28].z.value[0]+bv[20][29].z.value[0]+bv[20][30].z.value[0] == 12,
bv[21][1].z.value[0]+bv[21][2].z.value[0]+bv[21][3].z.value[0]+bv[21][4].z.value[0]+bv[21][5].z.value[0]+bv[21][6].z.value[0]+bv[21][7].z.value[0]+bv[21][8].z.value[0]+bv[21][9].z.value[0]+bv[21][10].z.value[0]+bv[21][11].z.value[0]+bv[21][12].z.value[0]+bv[21][13].z.value[0]+bv[21][14].z.value[0]+bv[21][15].z.value[0]+bv[21][16].z.value[0]+bv[21][17].z.value[0]+bv[21][18].z.value[0]+bv[21][19].z.value[0]+bv[21][20].z.value[0]+bv[21][21].z.value[0]+bv[21][22].z.value[0]+bv[21][23].z.value[0]+bv[21][24].z.value[0]+bv[21][25].z.value[0]+bv[21][26].z.value[0]+bv[21][27].z.value[0]+bv[21][28].z.value[0]+bv[21][29].z.value[0]+bv[21][30].z.value[0] == 7,
bv[22][1].z.value[0]+bv[22][2].z.value[0]+bv[22][3].z.value[0]+bv[22][4].z.value[0]+bv[22][5].z.value[0]+bv[22][6].z.value[0]+bv[22][7].z.value[0]+bv[22][8].z.value[0]+bv[22][9].z.value[0]+bv[22][10].z.value[0]+bv[22][11].z.value[0]+bv[22][12].z.value[0]+bv[22][13].z.value[0]+bv[22][14].z.value[0]+bv[22][15].z.value[0]+bv[22][16].z.value[0]+bv[22][17].z.value[0]+bv[22][18].z.value[0]+bv[22][19].z.value[0]+bv[22][20].z.value[0]+bv[22][21].z.value[0]+bv[22][22].z.value[0]+bv[22][23].z.value[0]+bv[22][24].z.value[0]+bv[22][25].z.value[0]+bv[22][26].z.value[0]+bv[22][27].z.value[0]+bv[22][28].z.value[0]+bv[22][29].z.value[0]+bv[22][30].z.value[0] == 14,
bv[23][1].z.value[0]+bv[23][2].z.value[0]+bv[23][3].z.value[0]+bv[23][4].z.value[0]+bv[23][5].z.value[0]+bv[23][6].z.value[0]+bv[23][7].z.value[0]+bv[23][8].z.value[0]+bv[23][9].z.value[0]+bv[23][10].z.value[0]+bv[23][11].z.value[0]+bv[23][12].z.value[0]+bv[23][13].z.value[0]+bv[23][14].z.value[0]+bv[23][15].z.value[0]+bv[23][16].z.value[0]+bv[23][17].z.value[0]+bv[23][18].z.value[0]+bv[23][19].z.value[0]+bv[23][20].z.value[0]+bv[23][21].z.value[0]+bv[23][22].z.value[0]+bv[23][23].z.value[0]+bv[23][24].z.value[0]+bv[23][25].z.value[0]+bv[23][26].z.value[0]+bv[23][27].z.value[0]+bv[23][28].z.value[0]+bv[23][29].z.value[0]+bv[23][30].z.value[0] == 11,
bv[24][1].z.value[0]+bv[24][2].z.value[0]+bv[24][3].z.value[0]+bv[24][4].z.value[0]+bv[24][5].z.value[0]+bv[24][6].z.value[0]+bv[24][7].z.value[0]+bv[24][8].z.value[0]+bv[24][9].z.value[0]+bv[24][10].z.value[0]+bv[24][11].z.value[0]+bv[24][12].z.value[0]+bv[24][13].z.value[0]+bv[24][14].z.value[0]+bv[24][15].z.value[0]+bv[24][16].z.value[0]+bv[24][17].z.value[0]+bv[24][18].z.value[0]+bv[24][19].z.value[0]+bv[24][20].z.value[0]+bv[24][21].z.value[0]+bv[24][22].z.value[0]+bv[24][23].z.value[0]+bv[24][24].z.value[0]+bv[24][25].z.value[0]+bv[24][26].z.value[0]+bv[24][27].z.value[0]+bv[24][28].z.value[0]+bv[24][29].z.value[0]+bv[24][30].z.value[0] == 4,
bv[25][1].z.value[0]+bv[25][2].z.value[0]+bv[25][3].z.value[0]+bv[25][4].z.value[0]+bv[25][5].z.value[0]+bv[25][6].z.value[0]+bv[25][7].z.value[0]+bv[25][8].z.value[0]+bv[25][9].z.value[0]+bv[25][10].z.value[0]+bv[25][11].z.value[0]+bv[25][12].z.value[0]+bv[25][13].z.value[0]+bv[25][14].z.value[0]+bv[25][15].z.value[0]+bv[25][16].z.value[0]+bv[25][17].z.value[0]+bv[25][18].z.value[0]+bv[25][19].z.value[0]+bv[25][20].z.value[0]+bv[25][21].z.value[0]+bv[25][22].z.value[0]+bv[25][23].z.value[0]+bv[25][24].z.value[0]+bv[25][25].z.value[0]+bv[25][26].z.value[0]+bv[25][27].z.value[0]+bv[25][28].z.value[0]+bv[25][29].z.value[0]+bv[25][30].z.value[0] == 10,
bv[1][1].z.value[0]+bv[2][1].z.value[0]+bv[3][1].z.value[0]+bv[4][1].z.value[0]+bv[5][1].z.value[0]+bv[6][1].z.value[0]+bv[7][1].z.value[0]+bv[8][1].z.value[0]+bv[9][1].z.value[0]+bv[10][1].z.value[0]+bv[11][1].z.value[0]+bv[12][1].z.value[0]+bv[13][1].z.value[0]+bv[14][1].z.value[0]+bv[15][1].z.value[0]+bv[16][1].z.value[0]+bv[17][1].z.value[0]+bv[18][1].z.value[0]+bv[19][1].z.value[0]+bv[20][1].z.value[0]+bv[21][1].z.value[0]+bv[22][1].z.value[0]+bv[23][1].z.value[0]+bv[24][1].z.value[0]+bv[25][1].z.value[0] == 2,
bv[1][2].z.value[0]+bv[2][2].z.value[0]+bv[3][2].z.value[0]+bv[4][2].z.value[0]+bv[5][2].z.value[0]+bv[6][2].z.value[0]+bv[7][2].z.value[0]+bv[8][2].z.value[0]+bv[9][2].z.value[0]+bv[10][2].z.value[0]+bv[11][2].z.value[0]+bv[12][2].z.value[0]+bv[13][2].z.value[0]+bv[14][2].z.value[0]+bv[15][2].z.value[0]+bv[16][2].z.value[0]+bv[17][2].z.value[0]+bv[18][2].z.value[0]+bv[19][2].z.value[0]+bv[20][2].z.value[0]+bv[21][2].z.value[0]+bv[22][2].z.value[0]+bv[23][2].z.value[0]+bv[24][2].z.value[0]+bv[25][2].z.value[0] == 2,
bv[1][3].z.value[0]+bv[2][3].z.value[0]+bv[3][3].z.value[0]+bv[4][3].z.value[0]+bv[5][3].z.value[0]+bv[6][3].z.value[0]+bv[7][3].z.value[0]+bv[8][3].z.value[0]+bv[9][3].z.value[0]+bv[10][3].z.value[0]+bv[11][3].z.value[0]+bv[12][3].z.value[0]+bv[13][3].z.value[0]+bv[14][3].z.value[0]+bv[15][3].z.value[0]+bv[16][3].z.value[0]+bv[17][3].z.value[0]+bv[18][3].z.value[0]+bv[19][3].z.value[0]+bv[20][3].z.value[0]+bv[21][3].z.value[0]+bv[22][3].z.value[0]+bv[23][3].z.value[0]+bv[24][3].z.value[0]+bv[25][3].z.value[0] == 2,
bv[1][4].z.value[0]+bv[2][4].z.value[0]+bv[3][4].z.value[0]+bv[4][4].z.value[0]+bv[5][4].z.value[0]+bv[6][4].z.value[0]+bv[7][4].z.value[0]+bv[8][4].z.value[0]+bv[9][4].z.value[0]+bv[10][4].z.value[0]+bv[11][4].z.value[0]+bv[12][4].z.value[0]+bv[13][4].z.value[0]+bv[14][4].z.value[0]+bv[15][4].z.value[0]+bv[16][4].z.value[0]+bv[17][4].z.value[0]+bv[18][4].z.value[0]+bv[19][4].z.value[0]+bv[20][4].z.value[0]+bv[21][4].z.value[0]+bv[22][4].z.value[0]+bv[23][4].z.value[0]+bv[24][4].z.value[0]+bv[25][4].z.value[0] == 10,
bv[1][5].z.value[0]+bv[2][5].z.value[0]+bv[3][5].z.value[0]+bv[4][5].z.value[0]+bv[5][5].z.value[0]+bv[6][5].z.value[0]+bv[7][5].z.value[0]+bv[8][5].z.value[0]+bv[9][5].z.value[0]+bv[10][5].z.value[0]+bv[11][5].z.value[0]+bv[12][5].z.value[0]+bv[13][5].z.value[0]+bv[14][5].z.value[0]+bv[15][5].z.value[0]+bv[16][5].z.value[0]+bv[17][5].z.value[0]+bv[18][5].z.value[0]+bv[19][5].z.value[0]+bv[20][5].z.value[0]+bv[21][5].z.value[0]+bv[22][5].z.value[0]+bv[23][5].z.value[0]+bv[24][5].z.value[0]+bv[25][5].z.value[0] == 8,
bv[1][6].z.value[0]+bv[2][6].z.value[0]+bv[3][6].z.value[0]+bv[4][6].z.value[0]+bv[5][6].z.value[0]+bv[6][6].z.value[0]+bv[7][6].z.value[0]+bv[8][6].z.value[0]+bv[9][6].z.value[0]+bv[10][6].z.value[0]+bv[11][6].z.value[0]+bv[12][6].z.value[0]+bv[13][6].z.value[0]+bv[14][6].z.value[0]+bv[15][6].z.value[0]+bv[16][6].z.value[0]+bv[17][6].z.value[0]+bv[18][6].z.value[0]+bv[19][6].z.value[0]+bv[20][6].z.value[0]+bv[21][6].z.value[0]+bv[22][6].z.value[0]+bv[23][6].z.value[0]+bv[24][6].z.value[0]+bv[25][6].z.value[0] == 10,
bv[1][7].z.value[0]+bv[2][7].z.value[0]+bv[3][7].z.value[0]+bv[4][7].z.value[0]+bv[5][7].z.value[0]+bv[6][7].z.value[0]+bv[7][7].z.value[0]+bv[8][7].z.value[0]+bv[9][7].z.value[0]+bv[10][7].z.value[0]+bv[11][7].z.value[0]+bv[12][7].z.value[0]+bv[13][7].z.value[0]+bv[14][7].z.value[0]+bv[15][7].z.value[0]+bv[16][7].z.value[0]+bv[17][7].z.value[0]+bv[18][7].z.value[0]+bv[19][7].z.value[0]+bv[20][7].z.value[0]+bv[21][7].z.value[0]+bv[22][7].z.value[0]+bv[23][7].z.value[0]+bv[24][7].z.value[0]+bv[25][7].z.value[0] == 4,
bv[1][8].z.value[0]+bv[2][8].z.value[0]+bv[3][8].z.value[0]+bv[4][8].z.value[0]+bv[5][8].z.value[0]+bv[6][8].z.value[0]+bv[7][8].z.value[0]+bv[8][8].z.value[0]+bv[9][8].z.value[0]+bv[10][8].z.value[0]+bv[11][8].z.value[0]+bv[12][8].z.value[0]+bv[13][8].z.value[0]+bv[14][8].z.value[0]+bv[15][8].z.value[0]+bv[16][8].z.value[0]+bv[17][8].z.value[0]+bv[18][8].z.value[0]+bv[19][8].z.value[0]+bv[20][8].z.value[0]+bv[21][8].z.value[0]+bv[22][8].z.value[0]+bv[23][8].z.value[0]+bv[24][8].z.value[0]+bv[25][8].z.value[0] == 6,
bv[1][9].z.value[0]+bv[2][9].z.value[0]+bv[3][9].z.value[0]+bv[4][9].z.value[0]+bv[5][9].z.value[0]+bv[6][9].z.value[0]+bv[7][9].z.value[0]+bv[8][9].z.value[0]+bv[9][9].z.value[0]+bv[10][9].z.value[0]+bv[11][9].z.value[0]+bv[12][9].z.value[0]+bv[13][9].z.value[0]+bv[14][9].z.value[0]+bv[15][9].z.value[0]+bv[16][9].z.value[0]+bv[17][9].z.value[0]+bv[18][9].z.value[0]+bv[19][9].z.value[0]+bv[20][9].z.value[0]+bv[21][9].z.value[0]+bv[22][9].z.value[0]+bv[23][9].z.value[0]+bv[24][9].z.value[0]+bv[25][9].z.value[0] == 9,
bv[1][10].z.value[0]+bv[2][10].z.value[0]+bv[3][10].z.value[0]+bv[4][10].z.value[0]+bv[5][10].z.value[0]+bv[6][10].z.value[0]+bv[7][10].z.value[0]+bv[8][10].z.value[0]+bv[9][10].z.value[0]+bv[10][10].z.value[0]+bv[11][10].z.value[0]+bv[12][10].z.value[0]+bv[13][10].z.value[0]+bv[14][10].z.value[0]+bv[15][10].z.value[0]+bv[16][10].z.value[0]+bv[17][10].z.value[0]+bv[18][10].z.value[0]+bv[19][10].z.value[0]+bv[20][10].z.value[0]+bv[21][10].z.value[0]+bv[22][10].z.value[0]+bv[23][10].z.value[0]+bv[24][10].z.value[0]+bv[25][10].z.value[0] == 7,
bv[1][11].z.value[0]+bv[2][11].z.value[0]+bv[3][11].z.value[0]+bv[4][11].z.value[0]+bv[5][11].z.value[0]+bv[6][11].z.value[0]+bv[7][11].z.value[0]+bv[8][11].z.value[0]+bv[9][11].z.value[0]+bv[10][11].z.value[0]+bv[11][11].z.value[0]+bv[12][11].z.value[0]+bv[13][11].z.value[0]+bv[14][11].z.value[0]+bv[15][11].z.value[0]+bv[16][11].z.value[0]+bv[17][11].z.value[0]+bv[18][11].z.value[0]+bv[19][11].z.value[0]+bv[20][11].z.value[0]+bv[21][11].z.value[0]+bv[22][11].z.value[0]+bv[23][11].z.value[0]+bv[24][11].z.value[0]+bv[25][11].z.value[0] == 5,
bv[1][12].z.value[0]+bv[2][12].z.value[0]+bv[3][12].z.value[0]+bv[4][12].z.value[0]+bv[5][12].z.value[0]+bv[6][12].z.value[0]+bv[7][12].z.value[0]+bv[8][12].z.value[0]+bv[9][12].z.value[0]+bv[10][12].z.value[0]+bv[11][12].z.value[0]+bv[12][12].z.value[0]+bv[13][12].z.value[0]+bv[14][12].z.value[0]+bv[15][12].z.value[0]+bv[16][12].z.value[0]+bv[17][12].z.value[0]+bv[18][12].z.value[0]+bv[19][12].z.value[0]+bv[20][12].z.value[0]+bv[21][12].z.value[0]+bv[22][12].z.value[0]+bv[23][12].z.value[0]+bv[24][12].z.value[0]+bv[25][12].z.value[0] == 7,
bv[1][13].z.value[0]+bv[2][13].z.value[0]+bv[3][13].z.value[0]+bv[4][13].z.value[0]+bv[5][13].z.value[0]+bv[6][13].z.value[0]+bv[7][13].z.value[0]+bv[8][13].z.value[0]+bv[9][13].z.value[0]+bv[10][13].z.value[0]+bv[11][13].z.value[0]+bv[12][13].z.value[0]+bv[13][13].z.value[0]+bv[14][13].z.value[0]+bv[15][13].z.value[0]+bv[16][13].z.value[0]+bv[17][13].z.value[0]+bv[18][13].z.value[0]+bv[19][13].z.value[0]+bv[20][13].z.value[0]+bv[21][13].z.value[0]+bv[22][13].z.value[0]+bv[23][13].z.value[0]+bv[24][13].z.value[0]+bv[25][13].z.value[0] == 6,
bv[1][14].z.value[0]+bv[2][14].z.value[0]+bv[3][14].z.value[0]+bv[4][14].z.value[0]+bv[5][14].z.value[0]+bv[6][14].z.value[0]+bv[7][14].z.value[0]+bv[8][14].z.value[0]+bv[9][14].z.value[0]+bv[10][14].z.value[0]+bv[11][14].z.value[0]+bv[12][14].z.value[0]+bv[13][14].z.value[0]+bv[14][14].z.value[0]+bv[15][14].z.value[0]+bv[16][14].z.value[0]+bv[17][14].z.value[0]+bv[18][14].z.value[0]+bv[19][14].z.value[0]+bv[20][14].z.value[0]+bv[21][14].z.value[0]+bv[22][14].z.value[0]+bv[23][14].z.value[0]+bv[24][14].z.value[0]+bv[25][14].z.value[0] == 8,
bv[1][15].z.value[0]+bv[2][15].z.value[0]+bv[3][15].z.value[0]+bv[4][15].z.value[0]+bv[5][15].z.value[0]+bv[6][15].z.value[0]+bv[7][15].z.value[0]+bv[8][15].z.value[0]+bv[9][15].z.value[0]+bv[10][15].z.value[0]+bv[11][15].z.value[0]+bv[12][15].z.value[0]+bv[13][15].z.value[0]+bv[14][15].z.value[0]+bv[15][15].z.value[0]+bv[16][15].z.value[0]+bv[17][15].z.value[0]+bv[18][15].z.value[0]+bv[19][15].z.value[0]+bv[20][15].z.value[0]+bv[21][15].z.value[0]+bv[22][15].z.value[0]+bv[23][15].z.value[0]+bv[24][15].z.value[0]+bv[25][15].z.value[0] == 5,
bv[1][16].z.value[0]+bv[2][16].z.value[0]+bv[3][16].z.value[0]+bv[4][16].z.value[0]+bv[5][16].z.value[0]+bv[6][16].z.value[0]+bv[7][16].z.value[0]+bv[8][16].z.value[0]+bv[9][16].z.value[0]+bv[10][16].z.value[0]+bv[11][16].z.value[0]+bv[12][16].z.value[0]+bv[13][16].z.value[0]+bv[14][16].z.value[0]+bv[15][16].z.value[0]+bv[16][16].z.value[0]+bv[17][16].z.value[0]+bv[18][16].z.value[0]+bv[19][16].z.value[0]+bv[20][16].z.value[0]+bv[21][16].z.value[0]+bv[22][16].z.value[0]+bv[23][16].z.value[0]+bv[24][16].z.value[0]+bv[25][16].z.value[0] == 7,
bv[1][17].z.value[0]+bv[2][17].z.value[0]+bv[3][17].z.value[0]+bv[4][17].z.value[0]+bv[5][17].z.value[0]+bv[6][17].z.value[0]+bv[7][17].z.value[0]+bv[8][17].z.value[0]+bv[9][17].z.value[0]+bv[10][17].z.value[0]+bv[11][17].z.value[0]+bv[12][17].z.value[0]+bv[13][17].z.value[0]+bv[14][17].z.value[0]+bv[15][17].z.value[0]+bv[16][17].z.value[0]+bv[17][17].z.value[0]+bv[18][17].z.value[0]+bv[19][17].z.value[0]+bv[20][17].z.value[0]+bv[21][17].z.value[0]+bv[22][17].z.value[0]+bv[23][17].z.value[0]+bv[24][17].z.value[0]+bv[25][17].z.value[0] == 4,
bv[1][18].z.value[0]+bv[2][18].z.value[0]+bv[3][18].z.value[0]+bv[4][18].z.value[0]+bv[5][18].z.value[0]+bv[6][18].z.value[0]+bv[7][18].z.value[0]+bv[8][18].z.value[0]+bv[9][18].z.value[0]+bv[10][18].z.value[0]+bv[11][18].z.value[0]+bv[12][18].z.value[0]+bv[13][18].z.value[0]+bv[14][18].z.value[0]+bv[15][18].z.value[0]+bv[16][18].z.value[0]+bv[17][18].z.value[0]+bv[18][18].z.value[0]+bv[19][18].z.value[0]+bv[20][18].z.value[0]+bv[21][18].z.value[0]+bv[22][18].z.value[0]+bv[23][18].z.value[0]+bv[24][18].z.value[0]+bv[25][18].z.value[0] == 6,
bv[1][19].z.value[0]+bv[2][19].z.value[0]+bv[3][19].z.value[0]+bv[4][19].z.value[0]+bv[5][19].z.value[0]+bv[6][19].z.value[0]+bv[7][19].z.value[0]+bv[8][19].z.value[0]+bv[9][19].z.value[0]+bv[10][19].z.value[0]+bv[11][19].z.value[0]+bv[12][19].z.value[0]+bv[13][19].z.value[0]+bv[14][19].z.value[0]+bv[15][19].z.value[0]+bv[16][19].z.value[0]+bv[17][19].z.value[0]+bv[18][19].z.value[0]+bv[19][19].z.value[0]+bv[20][19].z.value[0]+bv[21][19].z.value[0]+bv[22][19].z.value[0]+bv[23][19].z.value[0]+bv[24][19].z.value[0]+bv[25][19].z.value[0] == 7,
bv[1][20].z.value[0]+bv[2][20].z.value[0]+bv[3][20].z.value[0]+bv[4][20].z.value[0]+bv[5][20].z.value[0]+bv[6][20].z.value[0]+bv[7][20].z.value[0]+bv[8][20].z.value[0]+bv[9][20].z.value[0]+bv[10][20].z.value[0]+bv[11][20].z.value[0]+bv[12][20].z.value[0]+bv[13][20].z.value[0]+bv[14][20].z.value[0]+bv[15][20].z.value[0]+bv[16][20].z.value[0]+bv[17][20].z.value[0]+bv[18][20].z.value[0]+bv[19][20].z.value[0]+bv[20][20].z.value[0]+bv[21][20].z.value[0]+bv[22][20].z.value[0]+bv[23][20].z.value[0]+bv[24][20].z.value[0]+bv[25][20].z.value[0] == 6,
bv[1][21].z.value[0]+bv[2][21].z.value[0]+bv[3][21].z.value[0]+bv[4][21].z.value[0]+bv[5][21].z.value[0]+bv[6][21].z.value[0]+bv[7][21].z.value[0]+bv[8][21].z.value[0]+bv[9][21].z.value[0]+bv[10][21].z.value[0]+bv[11][21].z.value[0]+bv[12][21].z.value[0]+bv[13][21].z.value[0]+bv[14][21].z.value[0]+bv[15][21].z.value[0]+bv[16][21].z.value[0]+bv[17][21].z.value[0]+bv[18][21].z.value[0]+bv[19][21].z.value[0]+bv[20][21].z.value[0]+bv[21][21].z.value[0]+bv[22][21].z.value[0]+bv[23][21].z.value[0]+bv[24][21].z.value[0]+bv[25][21].z.value[0] == 6,
bv[1][22].z.value[0]+bv[2][22].z.value[0]+bv[3][22].z.value[0]+bv[4][22].z.value[0]+bv[5][22].z.value[0]+bv[6][22].z.value[0]+bv[7][22].z.value[0]+bv[8][22].z.value[0]+bv[9][22].z.value[0]+bv[10][22].z.value[0]+bv[11][22].z.value[0]+bv[12][22].z.value[0]+bv[13][22].z.value[0]+bv[14][22].z.value[0]+bv[15][22].z.value[0]+bv[16][22].z.value[0]+bv[17][22].z.value[0]+bv[18][22].z.value[0]+bv[19][22].z.value[0]+bv[20][22].z.value[0]+bv[21][22].z.value[0]+bv[22][22].z.value[0]+bv[23][22].z.value[0]+bv[24][22].z.value[0]+bv[25][22].z.value[0] == 11,
bv[1][23].z.value[0]+bv[2][23].z.value[0]+bv[3][23].z.value[0]+bv[4][23].z.value[0]+bv[5][23].z.value[0]+bv[6][23].z.value[0]+bv[7][23].z.value[0]+bv[8][23].z.value[0]+bv[9][23].z.value[0]+bv[10][23].z.value[0]+bv[11][23].z.value[0]+bv[12][23].z.value[0]+bv[13][23].z.value[0]+bv[14][23].z.value[0]+bv[15][23].z.value[0]+bv[16][23].z.value[0]+bv[17][23].z.value[0]+bv[18][23].z.value[0]+bv[19][23].z.value[0]+bv[20][23].z.value[0]+bv[21][23].z.value[0]+bv[22][23].z.value[0]+bv[23][23].z.value[0]+bv[24][23].z.value[0]+bv[25][23].z.value[0] == 5,
bv[1][24].z.value[0]+bv[2][24].z.value[0]+bv[3][24].z.value[0]+bv[4][24].z.value[0]+bv[5][24].z.value[0]+bv[6][24].z.value[0]+bv[7][24].z.value[0]+bv[8][24].z.value[0]+bv[9][24].z.value[0]+bv[10][24].z.value[0]+bv[11][24].z.value[0]+bv[12][24].z.value[0]+bv[13][24].z.value[0]+bv[14][24].z.value[0]+bv[15][24].z.value[0]+bv[16][24].z.value[0]+bv[17][24].z.value[0]+bv[18][24].z.value[0]+bv[19][24].z.value[0]+bv[20][24].z.value[0]+bv[21][24].z.value[0]+bv[22][24].z.value[0]+bv[23][24].z.value[0]+bv[24][24].z.value[0]+bv[25][24].z.value[0] == 7,
bv[1][25].z.value[0]+bv[2][25].z.value[0]+bv[3][25].z.value[0]+bv[4][25].z.value[0]+bv[5][25].z.value[0]+bv[6][25].z.value[0]+bv[7][25].z.value[0]+bv[8][25].z.value[0]+bv[9][25].z.value[0]+bv[10][25].z.value[0]+bv[11][25].z.value[0]+bv[12][25].z.value[0]+bv[13][25].z.value[0]+bv[14][25].z.value[0]+bv[15][25].z.value[0]+bv[16][25].z.value[0]+bv[17][25].z.value[0]+bv[18][25].z.value[0]+bv[19][25].z.value[0]+bv[20][25].z.value[0]+bv[21][25].z.value[0]+bv[22][25].z.value[0]+bv[23][25].z.value[0]+bv[24][25].z.value[0]+bv[25][25].z.value[0] == 6,
bv[1][26].z.value[0]+bv[2][26].z.value[0]+bv[3][26].z.value[0]+bv[4][26].z.value[0]+bv[5][26].z.value[0]+bv[6][26].z.value[0]+bv[7][26].z.value[0]+bv[8][26].z.value[0]+bv[9][26].z.value[0]+bv[10][26].z.value[0]+bv[11][26].z.value[0]+bv[12][26].z.value[0]+bv[13][26].z.value[0]+bv[14][26].z.value[0]+bv[15][26].z.value[0]+bv[16][26].z.value[0]+bv[17][26].z.value[0]+bv[18][26].z.value[0]+bv[19][26].z.value[0]+bv[20][26].z.value[0]+bv[21][26].z.value[0]+bv[22][26].z.value[0]+bv[23][26].z.value[0]+bv[24][26].z.value[0]+bv[25][26].z.value[0] == 8,
bv[1][27].z.value[0]+bv[2][27].z.value[0]+bv[3][27].z.value[0]+bv[4][27].z.value[0]+bv[5][27].z.value[0]+bv[6][27].z.value[0]+bv[7][27].z.value[0]+bv[8][27].z.value[0]+bv[9][27].z.value[0]+bv[10][27].z.value[0]+bv[11][27].z.value[0]+bv[12][27].z.value[0]+bv[13][27].z.value[0]+bv[14][27].z.value[0]+bv[15][27].z.value[0]+bv[16][27].z.value[0]+bv[17][27].z.value[0]+bv[18][27].z.value[0]+bv[19][27].z.value[0]+bv[20][27].z.value[0]+bv[21][27].z.value[0]+bv[22][27].z.value[0]+bv[23][27].z.value[0]+bv[24][27].z.value[0]+bv[25][27].z.value[0] == 7,
bv[1][28].z.value[0]+bv[2][28].z.value[0]+bv[3][28].z.value[0]+bv[4][28].z.value[0]+bv[5][28].z.value[0]+bv[6][28].z.value[0]+bv[7][28].z.value[0]+bv[8][28].z.value[0]+bv[9][28].z.value[0]+bv[10][28].z.value[0]+bv[11][28].z.value[0]+bv[12][28].z.value[0]+bv[13][28].z.value[0]+bv[14][28].z.value[0]+bv[15][28].z.value[0]+bv[16][28].z.value[0]+bv[17][28].z.value[0]+bv[18][28].z.value[0]+bv[19][28].z.value[0]+bv[20][28].z.value[0]+bv[21][28].z.value[0]+bv[22][28].z.value[0]+bv[23][28].z.value[0]+bv[24][28].z.value[0]+bv[25][28].z.value[0] == 7,
bv[1][29].z.value[0]+bv[2][29].z.value[0]+bv[3][29].z.value[0]+bv[4][29].z.value[0]+bv[5][29].z.value[0]+bv[6][29].z.value[0]+bv[7][29].z.value[0]+bv[8][29].z.value[0]+bv[9][29].z.value[0]+bv[10][29].z.value[0]+bv[11][29].z.value[0]+bv[12][29].z.value[0]+bv[13][29].z.value[0]+bv[14][29].z.value[0]+bv[15][29].z.value[0]+bv[16][29].z.value[0]+bv[17][29].z.value[0]+bv[18][29].z.value[0]+bv[19][29].z.value[0]+bv[20][29].z.value[0]+bv[21][29].z.value[0]+bv[22][29].z.value[0]+bv[23][29].z.value[0]+bv[24][29].z.value[0]+bv[25][29].z.value[0] == 2,
bv[1][30].z.value[0]+bv[2][30].z.value[0]+bv[3][30].z.value[0]+bv[4][30].z.value[0]+bv[5][30].z.value[0]+bv[6][30].z.value[0]+bv[7][30].z.value[0]+bv[8][30].z.value[0]+bv[9][30].z.value[0]+bv[10][30].z.value[0]+bv[11][30].z.value[0]+bv[12][30].z.value[0]+bv[13][30].z.value[0]+bv[14][30].z.value[0]+bv[15][30].z.value[0]+bv[16][30].z.value[0]+bv[17][30].z.value[0]+bv[18][30].z.value[0]+bv[19][30].z.value[0]+bv[20][30].z.value[0]+bv[21][30].z.value[0]+bv[22][30].z.value[0]+bv[23][30].z.value[0]+bv[24][30].z.value[0]+bv[25][30].z.value[0] == 2,
bv[1][1].z.value[0] == 0,
bv[1][2].z.value[0]+bv[2][1].z.value[0] == 0,
bv[1][3].z.value[0]+bv[2][2].z.value[0]+bv[3][1].z.value[0] == 0,
bv[1][4].z.value[0]+bv[2][3].z.value[0]+bv[3][2].z.value[0]+bv[4][1].z.value[0] == 0,
bv[1][5].z.value[0]+bv[2][4].z.value[0]+bv[3][3].z.value[0]+bv[4][2].z.value[0]+bv[5][1].z.value[0] == 0,
bv[1][6].z.value[0]+bv[2][5].z.value[0]+bv[3][4].z.value[0]+bv[4][3].z.value[0]+bv[5][2].z.value[0]+bv[6][1].z.value[0] == 1,
bv[1][7].z.value[0]+bv[2][6].z.value[0]+bv[3][5].z.value[0]+bv[4][4].z.value[0]+bv[5][3].z.value[0]+bv[6][2].z.value[0]+bv[7][1].z.value[0] == 3,
bv[1][8].z.value[0]+bv[2][7].z.value[0]+bv[3][6].z.value[0]+bv[4][5].z.value[0]+bv[5][4].z.value[0]+bv[6][3].z.value[0]+bv[7][2].z.value[0]+bv[8][1].z.value[0] == 2,
bv[1][9].z.value[0]+bv[2][8].z.value[0]+bv[3][7].z.value[0]+bv[4][6].z.value[0]+bv[5][5].z.value[0]+bv[6][4].z.value[0]+bv[7][3].z.value[0]+bv[8][2].z.value[0]+bv[9][1].z.value[0] == 2,
bv[1][10].z.value[0]+bv[2][9].z.value[0]+bv[3][8].z.value[0]+bv[4][7].z.value[0]+bv[5][6].z.value[0]+bv[6][5].z.value[0]+bv[7][4].z.value[0]+bv[8][3].z.value[0]+bv[9][2].z.value[0]+bv[10][1].z.value[0] == 3,
bv[1][11].z.value[0]+bv[2][10].z.value[0]+bv[3][9].z.value[0]+bv[4][8].z.value[0]+bv[5][7].z.value[0]+bv[6][6].z.value[0]+bv[7][5].z.value[0]+bv[8][4].z.value[0]+bv[9][3].z.value[0]+bv[10][2].z.value[0]+bv[11][1].z.value[0] == 3,
bv[1][12].z.value[0]+bv[2][11].z.value[0]+bv[3][10].z.value[0]+bv[4][9].z.value[0]+bv[5][8].z.value[0]+bv[6][7].z.value[0]+bv[7][6].z.value[0]+bv[8][5].z.value[0]+bv[9][4].z.value[0]+bv[10][3].z.value[0]+bv[11][2].z.value[0]+bv[12][1].z.value[0] == 3,
bv[1][13].z.value[0]+bv[2][12].z.value[0]+bv[3][11].z.value[0]+bv[4][10].z.value[0]+bv[5][9].z.value[0]+bv[6][8].z.value[0]+bv[7][7].z.value[0]+bv[8][6].z.value[0]+bv[9][5].z.value[0]+bv[10][4].z.value[0]+bv[11][3].z.value[0]+bv[12][2].z.value[0]+bv[13][1].z.value[0] == 1,
bv[1][14].z.value[0]+bv[2][13].z.value[0]+bv[3][12].z.value[0]+bv[4][11].z.value[0]+bv[5][10].z.value[0]+bv[6][9].z.value[0]+bv[7][8].z.value[0]+bv[8][7].z.value[0]+bv[9][6].z.value[0]+bv[10][5].z.value[0]+bv[11][4].z.value[0]+bv[12][3].z.value[0]+bv[13][2].z.value[0]+bv[14][1].z.value[0] == 4,
bv[1][15].z.value[0]+bv[2][14].z.value[0]+bv[3][13].z.value[0]+bv[4][12].z.value[0]+bv[5][11].z.value[0]+bv[6][10].z.value[0]+bv[7][9].z.value[0]+bv[8][8].z.value[0]+bv[9][7].z.value[0]+bv[10][6].z.value[0]+bv[11][5].z.value[0]+bv[12][4].z.value[0]+bv[13][3].z.value[0]+bv[14][2].z.value[0]+bv[15][1].z.value[0] == 3,
bv[1][16].z.value[0]+bv[2][15].z.value[0]+bv[3][14].z.value[0]+bv[4][13].z.value[0]+bv[5][12].z.value[0]+bv[6][11].z.value[0]+bv[7][10].z.value[0]+bv[8][9].z.value[0]+bv[9][8].z.value[0]+bv[10][7].z.value[0]+bv[11][6].z.value[0]+bv[12][5].z.value[0]+bv[13][4].z.value[0]+bv[14][3].z.value[0]+bv[15][2].z.value[0]+bv[16][1].z.value[0] == 3,
bv[1][17].z.value[0]+bv[2][16].z.value[0]+bv[3][15].z.value[0]+bv[4][14].z.value[0]+bv[5][13].z.value[0]+bv[6][12].z.value[0]+bv[7][11].z.value[0]+bv[8][10].z.value[0]+bv[9][9].z.value[0]+bv[10][8].z.value[0]+bv[11][7].z.value[0]+bv[12][6].z.value[0]+bv[13][5].z.value[0]+bv[14][4].z.value[0]+bv[15][3].z.value[0]+bv[16][2].z.value[0]+bv[17][1].z.value[0] == 4,
bv[1][18].z.value[0]+bv[2][17].z.value[0]+bv[3][16].z.value[0]+bv[4][15].z.value[0]+bv[5][14].z.value[0]+bv[6][13].z.value[0]+bv[7][12].z.value[0]+bv[8][11].z.value[0]+bv[9][10].z.value[0]+bv[10][9].z.value[0]+bv[11][8].z.value[0]+bv[12][7].z.value[0]+bv[13][6].z.value[0]+bv[14][5].z.value[0]+bv[15][4].z.value[0]+bv[16][3].z.value[0]+bv[17][2].z.value[0]+bv[18][1].z.value[0] == 5,
bv[1][19].z.value[0]+bv[2][18].z.value[0]+bv[3][17].z.value[0]+bv[4][16].z.value[0]+bv[5][15].z.value[0]+bv[6][14].z.value[0]+bv[7][13].z.value[0]+bv[8][12].z.value[0]+bv[9][11].z.value[0]+bv[10][10].z.value[0]+bv[11][9].z.value[0]+bv[12][8].z.value[0]+bv[13][7].z.value[0]+bv[14][6].z.value[0]+bv[15][5].z.value[0]+bv[16][4].z.value[0]+bv[17][3].z.value[0]+bv[18][2].z.value[0]+bv[19][1].z.value[0] == 3,
bv[1][20].z.value[0]+bv[2][19].z.value[0]+bv[3][18].z.value[0]+bv[4][17].z.value[0]+bv[5][16].z.value[0]+bv[6][15].z.value[0]+bv[7][14].z.value[0]+bv[8][13].z.value[0]+bv[9][12].z.value[0]+bv[10][11].z.value[0]+bv[11][10].z.value[0]+bv[12][9].z.value[0]+bv[13][8].z.value[0]+bv[14][7].z.value[0]+bv[15][6].z.value[0]+bv[16][5].z.value[0]+bv[17][4].z.value[0]+bv[18][3].z.value[0]+bv[19][2].z.value[0]+bv[20][1].z.value[0] == 5,
bv[1][21].z.value[0]+bv[2][20].z.value[0]+bv[3][19].z.value[0]+bv[4][18].z.value[0]+bv[5][17].z.value[0]+bv[6][16].z.value[0]+bv[7][15].z.value[0]+bv[8][14].z.value[0]+bv[9][13].z.value[0]+bv[10][12].z.value[0]+bv[11][11].z.value[0]+bv[12][10].z.value[0]+bv[13][9].z.value[0]+bv[14][8].z.value[0]+bv[15][7].z.value[0]+bv[16][6].z.value[0]+bv[17][5].z.value[0]+bv[18][4].z.value[0]+bv[19][3].z.value[0]+bv[20][2].z.value[0]+bv[21][1].z.value[0] == 5,
bv[1][22].z.value[0]+bv[2][21].z.value[0]+bv[3][20].z.value[0]+bv[4][19].z.value[0]+bv[5][18].z.value[0]+bv[6][17].z.value[0]+bv[7][16].z.value[0]+bv[8][15].z.value[0]+bv[9][14].z.value[0]+bv[10][13].z.value[0]+bv[11][12].z.value[0]+bv[12][11].z.value[0]+bv[13][10].z.value[0]+bv[14][9].z.value[0]+bv[15][8].z.value[0]+bv[16][7].z.value[0]+bv[17][6].z.value[0]+bv[18][5].z.value[0]+bv[19][4].z.value[0]+bv[20][3].z.value[0]+bv[21][2].z.value[0]+bv[22][1].z.value[0] == 6,
bv[1][23].z.value[0]+bv[2][22].z.value[0]+bv[3][21].z.value[0]+bv[4][20].z.value[0]+bv[5][19].z.value[0]+bv[6][18].z.value[0]+bv[7][17].z.value[0]+bv[8][16].z.value[0]+bv[9][15].z.value[0]+bv[10][14].z.value[0]+bv[11][13].z.value[0]+bv[12][12].z.value[0]+bv[13][11].z.value[0]+bv[14][10].z.value[0]+bv[15][9].z.value[0]+bv[16][8].z.value[0]+bv[17][7].z.value[0]+bv[18][6].z.value[0]+bv[19][5].z.value[0]+bv[20][4].z.value[0]+bv[21][3].z.value[0]+bv[22][2].z.value[0]+bv[23][1].z.value[0] == 3,
bv[1][24].z.value[0]+bv[2][23].z.value[0]+bv[3][22].z.value[0]+bv[4][21].z.value[0]+bv[5][20].z.value[0]+bv[6][19].z.value[0]+bv[7][18].z.value[0]+bv[8][17].z.value[0]+bv[9][16].z.value[0]+bv[10][15].z.value[0]+bv[11][14].z.value[0]+bv[12][13].z.value[0]+bv[13][12].z.value[0]+bv[14][11].z.value[0]+bv[15][10].z.value[0]+bv[16][9].z.value[0]+bv[17][8].z.value[0]+bv[18][7].z.value[0]+bv[19][6].z.value[0]+bv[20][5].z.value[0]+bv[21][4].z.value[0]+bv[22][3].z.value[0]+bv[23][2].z.value[0]+bv[24][1].z.value[0] == 8,
bv[1][25].z.value[0]+bv[2][24].z.value[0]+bv[3][23].z.value[0]+bv[4][22].z.value[0]+bv[5][21].z.value[0]+bv[6][20].z.value[0]+bv[7][19].z.value[0]+bv[8][18].z.value[0]+bv[9][17].z.value[0]+bv[10][16].z.value[0]+bv[11][15].z.value[0]+bv[12][14].z.value[0]+bv[13][13].z.value[0]+bv[14][12].z.value[0]+bv[15][11].z.value[0]+bv[16][10].z.value[0]+bv[17][9].z.value[0]+bv[18][8].z.value[0]+bv[19][7].z.value[0]+bv[20][6].z.value[0]+bv[21][5].z.value[0]+bv[22][4].z.value[0]+bv[23][3].z.value[0]+bv[24][2].z.value[0]+bv[25][1].z.value[0] == 5,
bv[1][26].z.value[0]+bv[2][25].z.value[0]+bv[3][24].z.value[0]+bv[4][23].z.value[0]+bv[5][22].z.value[0]+bv[6][21].z.value[0]+bv[7][20].z.value[0]+bv[8][19].z.value[0]+bv[9][18].z.value[0]+bv[10][17].z.value[0]+bv[11][16].z.value[0]+bv[12][15].z.value[0]+bv[13][14].z.value[0]+bv[14][13].z.value[0]+bv[15][12].z.value[0]+bv[16][11].z.value[0]+bv[17][10].z.value[0]+bv[18][9].z.value[0]+bv[19][8].z.value[0]+bv[20][7].z.value[0]+bv[21][6].z.value[0]+bv[22][5].z.value[0]+bv[23][4].z.value[0]+bv[24][3].z.value[0]+bv[25][2].z.value[0] == 3,
bv[1][27].z.value[0]+bv[2][26].z.value[0]+bv[3][25].z.value[0]+bv[4][24].z.value[0]+bv[5][23].z.value[0]+bv[6][22].z.value[0]+bv[7][21].z.value[0]+bv[8][20].z.value[0]+bv[9][19].z.value[0]+bv[10][18].z.value[0]+bv[11][17].z.value[0]+bv[12][16].z.value[0]+bv[13][15].z.value[0]+bv[14][14].z.value[0]+bv[15][13].z.value[0]+bv[16][12].z.value[0]+bv[17][11].z.value[0]+bv[18][10].z.value[0]+bv[19][9].z.value[0]+bv[20][8].z.value[0]+bv[21][7].z.value[0]+bv[22][6].z.value[0]+bv[23][5].z.value[0]+bv[24][4].z.value[0]+bv[25][3].z.value[0] == 2,
bv[1][28].z.value[0]+bv[2][27].z.value[0]+bv[3][26].z.value[0]+bv[4][25].z.value[0]+bv[5][24].z.value[0]+bv[6][23].z.value[0]+bv[7][22].z.value[0]+bv[8][21].z.value[0]+bv[9][20].z.value[0]+bv[10][19].z.value[0]+bv[11][18].z.value[0]+bv[12][17].z.value[0]+bv[13][16].z.value[0]+bv[14][15].z.value[0]+bv[15][14].z.value[0]+bv[16][13].z.value[0]+bv[17][12].z.value[0]+bv[18][11].z.value[0]+bv[19][10].z.value[0]+bv[20][9].z.value[0]+bv[21][8].z.value[0]+bv[22][7].z.value[0]+bv[23][6].z.value[0]+bv[24][5].z.value[0]+bv[25][4].z.value[0] == 4,
bv[1][29].z.value[0]+bv[2][28].z.value[0]+bv[3][27].z.value[0]+bv[4][26].z.value[0]+bv[5][25].z.value[0]+bv[6][24].z.value[0]+bv[7][23].z.value[0]+bv[8][22].z.value[0]+bv[9][21].z.value[0]+bv[10][20].z.value[0]+bv[11][19].z.value[0]+bv[12][18].z.value[0]+bv[13][17].z.value[0]+bv[14][16].z.value[0]+bv[15][15].z.value[0]+bv[16][14].z.value[0]+bv[17][13].z.value[0]+bv[18][12].z.value[0]+bv[19][11].z.value[0]+bv[20][10].z.value[0]+bv[21][9].z.value[0]+bv[22][8].z.value[0]+bv[23][7].z.value[0]+bv[24][6].z.value[0]+bv[25][5].z.value[0] == 5,
bv[1][30].z.value[0]+bv[2][29].z.value[0]+bv[3][28].z.value[0]+bv[4][27].z.value[0]+bv[5][26].z.value[0]+bv[6][25].z.value[0]+bv[7][24].z.value[0]+bv[8][23].z.value[0]+bv[9][22].z.value[0]+bv[10][21].z.value[0]+bv[11][20].z.value[0]+bv[12][19].z.value[0]+bv[13][18].z.value[0]+bv[14][17].z.value[0]+bv[15][16].z.value[0]+bv[16][15].z.value[0]+bv[17][14].z.value[0]+bv[18][13].z.value[0]+bv[19][12].z.value[0]+bv[20][11].z.value[0]+bv[21][10].z.value[0]+bv[22][9].z.value[0]+bv[23][8].z.value[0]+bv[24][7].z.value[0]+bv[25][6].z.value[0] == 7,
bv[2][30].z.value[0]+bv[3][29].z.value[0]+bv[4][28].z.value[0]+bv[5][27].z.value[0]+bv[6][26].z.value[0]+bv[7][25].z.value[0]+bv[8][24].z.value[0]+bv[9][23].z.value[0]+bv[10][22].z.value[0]+bv[11][21].z.value[0]+bv[12][20].z.value[0]+bv[13][19].z.value[0]+bv[14][18].z.value[0]+bv[15][17].z.value[0]+bv[16][16].z.value[0]+bv[17][15].z.value[0]+bv[18][14].z.value[0]+bv[19][13].z.value[0]+bv[20][12].z.value[0]+bv[21][11].z.value[0]+bv[22][10].z.value[0]+bv[23][9].z.value[0]+bv[24][8].z.value[0]+bv[25][7].z.value[0] == 7,
bv[3][30].z.value[0]+bv[4][29].z.value[0]+bv[5][28].z.value[0]+bv[6][27].z.value[0]+bv[7][26].z.value[0]+bv[8][25].z.value[0]+bv[9][24].z.value[0]+bv[10][23].z.value[0]+bv[11][22].z.value[0]+bv[12][21].z.value[0]+bv[13][20].z.value[0]+bv[14][19].z.value[0]+bv[15][18].z.value[0]+bv[16][17].z.value[0]+bv[17][16].z.value[0]+bv[18][15].z.value[0]+bv[19][14].z.value[0]+bv[20][13].z.value[0]+bv[21][12].z.value[0]+bv[22][11].z.value[0]+bv[23][10].z.value[0]+bv[24][9].z.value[0]+bv[25][8].z.value[0] == 7,
bv[4][30].z.value[0]+bv[5][29].z.value[0]+bv[6][28].z.value[0]+bv[7][27].z.value[0]+bv[8][26].z.value[0]+bv[9][25].z.value[0]+bv[10][24].z.value[0]+bv[11][23].z.value[0]+bv[12][22].z.value[0]+bv[13][21].z.value[0]+bv[14][20].z.value[0]+bv[15][19].z.value[0]+bv[16][18].z.value[0]+bv[17][17].z.value[0]+bv[18][16].z.value[0]+bv[19][15].z.value[0]+bv[20][14].z.value[0]+bv[21][13].z.value[0]+bv[22][12].z.value[0]+bv[23][11].z.value[0]+bv[24][10].z.value[0]+bv[25][9].z.value[0] == 7,
bv[5][30].z.value[0]+bv[6][29].z.value[0]+bv[7][28].z.value[0]+bv[8][27].z.value[0]+bv[9][26].z.value[0]+bv[10][25].z.value[0]+bv[11][24].z.value[0]+bv[12][23].z.value[0]+bv[13][22].z.value[0]+bv[14][21].z.value[0]+bv[15][20].z.value[0]+bv[16][19].z.value[0]+bv[17][18].z.value[0]+bv[18][17].z.value[0]+bv[19][16].z.value[0]+bv[20][15].z.value[0]+bv[21][14].z.value[0]+bv[22][13].z.value[0]+bv[23][12].z.value[0]+bv[24][11].z.value[0]+bv[25][10].z.value[0] == 7,
bv[6][30].z.value[0]+bv[7][29].z.value[0]+bv[8][28].z.value[0]+bv[9][27].z.value[0]+bv[10][26].z.value[0]+bv[11][25].z.value[0]+bv[12][24].z.value[0]+bv[13][23].z.value[0]+bv[14][22].z.value[0]+bv[15][21].z.value[0]+bv[16][20].z.value[0]+bv[17][19].z.value[0]+bv[18][18].z.value[0]+bv[19][17].z.value[0]+bv[20][16].z.value[0]+bv[21][15].z.value[0]+bv[22][14].z.value[0]+bv[23][13].z.value[0]+bv[24][12].z.value[0]+bv[25][11].z.value[0] == 4,
bv[7][30].z.value[0]+bv[8][29].z.value[0]+bv[9][28].z.value[0]+bv[10][27].z.value[0]+bv[11][26].z.value[0]+bv[12][25].z.value[0]+bv[13][24].z.value[0]+bv[14][23].z.value[0]+bv[15][22].z.value[0]+bv[16][21].z.value[0]+bv[17][20].z.value[0]+bv[18][19].z.value[0]+bv[19][18].z.value[0]+bv[20][17].z.value[0]+bv[21][16].z.value[0]+bv[22][15].z.value[0]+bv[23][14].z.value[0]+bv[24][13].z.value[0]+bv[25][12].z.value[0] == 4,
bv[8][30].z.value[0]+bv[9][29].z.value[0]+bv[10][28].z.value[0]+bv[11][27].z.value[0]+bv[12][26].z.value[0]+bv[13][25].z.value[0]+bv[14][24].z.value[0]+bv[15][23].z.value[0]+bv[16][22].z.value[0]+bv[17][21].z.value[0]+bv[18][20].z.value[0]+bv[19][19].z.value[0]+bv[20][18].z.value[0]+bv[21][17].z.value[0]+bv[22][16].z.value[0]+bv[23][15].z.value[0]+bv[24][14].z.value[0]+bv[25][13].z.value[0] == 4,
bv[9][30].z.value[0]+bv[10][29].z.value[0]+bv[11][28].z.value[0]+bv[12][27].z.value[0]+bv[13][26].z.value[0]+bv[14][25].z.value[0]+bv[15][24].z.value[0]+bv[16][23].z.value[0]+bv[17][22].z.value[0]+bv[18][21].z.value[0]+bv[19][20].z.value[0]+bv[20][19].z.value[0]+bv[21][18].z.value[0]+bv[22][17].z.value[0]+bv[23][16].z.value[0]+bv[24][15].z.value[0]+bv[25][14].z.value[0] == 4,
bv[10][30].z.value[0]+bv[11][29].z.value[0]+bv[12][28].z.value[0]+bv[13][27].z.value[0]+bv[14][26].z.value[0]+bv[15][25].z.value[0]+bv[16][24].z.value[0]+bv[17][23].z.value[0]+bv[18][22].z.value[0]+bv[19][21].z.value[0]+bv[20][20].z.value[0]+bv[21][19].z.value[0]+bv[22][18].z.value[0]+bv[23][17].z.value[0]+bv[24][16].z.value[0]+bv[25][15].z.value[0] == 4,
bv[11][30].z.value[0]+bv[12][29].z.value[0]+bv[13][28].z.value[0]+bv[14][27].z.value[0]+bv[15][26].z.value[0]+bv[16][25].z.value[0]+bv[17][24].z.value[0]+bv[18][23].z.value[0]+bv[19][22].z.value[0]+bv[20][21].z.value[0]+bv[21][20].z.value[0]+bv[22][19].z.value[0]+bv[23][18].z.value[0]+bv[24][17].z.value[0]+bv[25][16].z.value[0] == 4,
bv[12][30].z.value[0]+bv[13][29].z.value[0]+bv[14][28].z.value[0]+bv[15][27].z.value[0]+bv[16][26].z.value[0]+bv[17][25].z.value[0]+bv[18][24].z.value[0]+bv[19][23].z.value[0]+bv[20][22].z.value[0]+bv[21][21].z.value[0]+bv[22][20].z.value[0]+bv[23][19].z.value[0]+bv[24][18].z.value[0]+bv[25][17].z.value[0] == 6,
bv[13][30].z.value[0]+bv[14][29].z.value[0]+bv[15][28].z.value[0]+bv[16][27].z.value[0]+bv[17][26].z.value[0]+bv[18][25].z.value[0]+bv[19][24].z.value[0]+bv[20][23].z.value[0]+bv[21][22].z.value[0]+bv[22][21].z.value[0]+bv[23][20].z.value[0]+bv[24][19].z.value[0]+bv[25][18].z.value[0] == 5,
bv[14][30].z.value[0]+bv[15][29].z.value[0]+bv[16][28].z.value[0]+bv[17][27].z.value[0]+bv[18][26].z.value[0]+bv[19][25].z.value[0]+bv[20][24].z.value[0]+bv[21][23].z.value[0]+bv[22][22].z.value[0]+bv[23][21].z.value[0]+bv[24][20].z.value[0]+bv[25][19].z.value[0] == 6,
bv[15][30].z.value[0]+bv[16][29].z.value[0]+bv[17][28].z.value[0]+bv[18][27].z.value[0]+bv[19][26].z.value[0]+bv[20][25].z.value[0]+bv[21][24].z.value[0]+bv[22][23].z.value[0]+bv[23][22].z.value[0]+bv[24][21].z.value[0]+bv[25][20].z.value[0] == 4,
bv[16][30].z.value[0]+bv[17][29].z.value[0]+bv[18][28].z.value[0]+bv[19][27].z.value[0]+bv[20][26].z.value[0]+bv[21][25].z.value[0]+bv[22][24].z.value[0]+bv[23][23].z.value[0]+bv[24][22].z.value[0]+bv[25][21].z.value[0] == 5,
bv[17][30].z.value[0]+bv[18][29].z.value[0]+bv[19][28].z.value[0]+bv[20][27].z.value[0]+bv[21][26].z.value[0]+bv[22][25].z.value[0]+bv[23][24].z.value[0]+bv[24][23].z.value[0]+bv[25][22].z.value[0] == 5,
bv[18][30].z.value[0]+bv[19][29].z.value[0]+bv[20][28].z.value[0]+bv[21][27].z.value[0]+bv[22][26].z.value[0]+bv[23][25].z.value[0]+bv[24][24].z.value[0]+bv[25][23].z.value[0] == 4,
bv[19][30].z.value[0]+bv[20][29].z.value[0]+bv[21][28].z.value[0]+bv[22][27].z.value[0]+bv[23][26].z.value[0]+bv[24][25].z.value[0]+bv[25][24].z.value[0] == 1,
bv[20][30].z.value[0]+bv[21][29].z.value[0]+bv[22][28].z.value[0]+bv[23][27].z.value[0]+bv[24][26].z.value[0]+bv[25][25].z.value[0] == 1,
bv[21][30].z.value[0]+bv[22][29].z.value[0]+bv[23][28].z.value[0]+bv[24][27].z.value[0]+bv[25][26].z.value[0] == 0,
bv[22][30].z.value[0]+bv[23][29].z.value[0]+bv[24][28].z.value[0]+bv[25][27].z.value[0] == 0,
bv[23][30].z.value[0]+bv[24][29].z.value[0]+bv[25][28].z.value[0] == 0,
bv[24][30].z.value[0]+bv[25][29].z.value[0] == 0,
bv[25][30].z.value[0] == 0,
bv[1][30].z.value[0] == 0,
bv[1][29].z.value[0]+bv[2][30].z.value[0] == 0,
bv[1][28].z.value[0]+bv[2][29].z.value[0]+bv[3][30].z.value[0] == 0,
bv[1][27].z.value[0]+bv[2][28].z.value[0]+bv[3][29].z.value[0]+bv[4][30].z.value[0] == 0,
bv[1][26].z.value[0]+bv[2][27].z.value[0]+bv[3][28].z.value[0]+bv[4][29].z.value[0]+bv[5][30].z.value[0] == 0,
bv[1][25].z.value[0]+bv[2][26].z.value[0]+bv[3][27].z.value[0]+bv[4][28].z.value[0]+bv[5][29].z.value[0]+bv[6][30].z.value[0] == 0,
bv[1][24].z.value[0]+bv[2][25].z.value[0]+bv[3][26].z.value[0]+bv[4][27].z.value[0]+bv[5][28].z.value[0]+bv[6][29].z.value[0]+bv[7][30].z.value[0] == 1,
bv[1][23].z.value[0]+bv[2][24].z.value[0]+bv[3][25].z.value[0]+bv[4][26].z.value[0]+bv[5][27].z.value[0]+bv[6][28].z.value[0]+bv[7][29].z.value[0]+bv[8][30].z.value[0] == 2,
bv[1][22].z.value[0]+bv[2][23].z.value[0]+bv[3][24].z.value[0]+bv[4][25].z.value[0]+bv[5][26].z.value[0]+bv[6][27].z.value[0]+bv[7][28].z.value[0]+bv[8][29].z.value[0]+bv[9][30].z.value[0] == 3,
bv[1][21].z.value[0]+bv[2][22].z.value[0]+bv[3][23].z.value[0]+bv[4][24].z.value[0]+bv[5][25].z.value[0]+bv[6][26].z.value[0]+bv[7][27].z.value[0]+bv[8][28].z.value[0]+bv[9][29].z.value[0]+bv[10][30].z.value[0] == 1,
bv[1][20].z.value[0]+bv[2][21].z.value[0]+bv[3][22].z.value[0]+bv[4][23].z.value[0]+bv[5][24].z.value[0]+bv[6][25].z.value[0]+bv[7][26].z.value[0]+bv[8][27].z.value[0]+bv[9][28].z.value[0]+bv[10][29].z.value[0]+bv[11][30].z.value[0] == 2,
bv[1][19].z.value[0]+bv[2][20].z.value[0]+bv[3][21].z.value[0]+bv[4][22].z.value[0]+bv[5][23].z.value[0]+bv[6][24].z.value[0]+bv[7][25].z.value[0]+bv[8][26].z.value[0]+bv[9][27].z.value[0]+bv[10][28].z.value[0]+bv[11][29].z.value[0]+bv[12][30].z.value[0] == 3,
bv[1][18].z.value[0]+bv[2][19].z.value[0]+bv[3][20].z.value[0]+bv[4][21].z.value[0]+bv[5][22].z.value[0]+bv[6][23].z.value[0]+bv[7][24].z.value[0]+bv[8][25].z.value[0]+bv[9][26].z.value[0]+bv[10][27].z.value[0]+bv[11][28].z.value[0]+bv[12][29].z.value[0]+bv[13][30].z.value[0] == 4,
bv[1][17].z.value[0]+bv[2][18].z.value[0]+bv[3][19].z.value[0]+bv[4][20].z.value[0]+bv[5][21].z.value[0]+bv[6][22].z.value[0]+bv[7][23].z.value[0]+bv[8][24].z.value[0]+bv[9][25].z.value[0]+bv[10][26].z.value[0]+bv[11][27].z.value[0]+bv[12][28].z.value[0]+bv[13][29].z.value[0]+bv[14][30].z.value[0] == 3,
bv[1][16].z.value[0]+bv[2][17].z.value[0]+bv[3][18].z.value[0]+bv[4][19].z.value[0]+bv[5][20].z.value[0]+bv[6][21].z.value[0]+bv[7][22].z.value[0]+bv[8][23].z.value[0]+bv[9][24].z.value[0]+bv[10][25].z.value[0]+bv[11][26].z.value[0]+bv[12][27].z.value[0]+bv[13][28].z.value[0]+bv[14][29].z.value[0]+bv[15][30].z.value[0] == 5,
bv[1][15].z.value[0]+bv[2][16].z.value[0]+bv[3][17].z.value[0]+bv[4][18].z.value[0]+bv[5][19].z.value[0]+bv[6][20].z.value[0]+bv[7][21].z.value[0]+bv[8][22].z.value[0]+bv[9][23].z.value[0]+bv[10][24].z.value[0]+bv[11][25].z.value[0]+bv[12][26].z.value[0]+bv[13][27].z.value[0]+bv[14][28].z.value[0]+bv[15][29].z.value[0]+bv[16][30].z.value[0] == 5,
bv[1][14].z.value[0]+bv[2][15].z.value[0]+bv[3][16].z.value[0]+bv[4][17].z.value[0]+bv[5][18].z.value[0]+bv[6][19].z.value[0]+bv[7][20].z.value[0]+bv[8][21].z.value[0]+bv[9][22].z.value[0]+bv[10][23].z.value[0]+bv[11][24].z.value[0]+bv[12][25].z.value[0]+bv[13][26].z.value[0]+bv[14][27].z.value[0]+bv[15][28].z.value[0]+bv[16][29].z.value[0]+bv[17][30].z.value[0] == 3,
bv[1][13].z.value[0]+bv[2][14].z.value[0]+bv[3][15].z.value[0]+bv[4][16].z.value[0]+bv[5][17].z.value[0]+bv[6][18].z.value[0]+bv[7][19].z.value[0]+bv[8][20].z.value[0]+bv[9][21].z.value[0]+bv[10][22].z.value[0]+bv[11][23].z.value[0]+bv[12][24].z.value[0]+bv[13][25].z.value[0]+bv[14][26].z.value[0]+bv[15][27].z.value[0]+bv[16][28].z.value[0]+bv[17][29].z.value[0]+bv[18][30].z.value[0] == 3,
bv[1][12].z.value[0]+bv[2][13].z.value[0]+bv[3][14].z.value[0]+bv[4][15].z.value[0]+bv[5][16].z.value[0]+bv[6][17].z.value[0]+bv[7][18].z.value[0]+bv[8][19].z.value[0]+bv[9][20].z.value[0]+bv[10][21].z.value[0]+bv[11][22].z.value[0]+bv[12][23].z.value[0]+bv[13][24].z.value[0]+bv[14][25].z.value[0]+bv[15][26].z.value[0]+bv[16][27].z.value[0]+bv[17][28].z.value[0]+bv[18][29].z.value[0]+bv[19][30].z.value[0] == 2,
bv[1][11].z.value[0]+bv[2][12].z.value[0]+bv[3][13].z.value[0]+bv[4][14].z.value[0]+bv[5][15].z.value[0]+bv[6][16].z.value[0]+bv[7][17].z.value[0]+bv[8][18].z.value[0]+bv[9][19].z.value[0]+bv[10][20].z.value[0]+bv[11][21].z.value[0]+bv[12][22].z.value[0]+bv[13][23].z.value[0]+bv[14][24].z.value[0]+bv[15][25].z.value[0]+bv[16][26].z.value[0]+bv[17][27].z.value[0]+bv[18][28].z.value[0]+bv[19][29].z.value[0]+bv[20][30].z.value[0] == 4,
bv[1][10].z.value[0]+bv[2][11].z.value[0]+bv[3][12].z.value[0]+bv[4][13].z.value[0]+bv[5][14].z.value[0]+bv[6][15].z.value[0]+bv[7][16].z.value[0]+bv[8][17].z.value[0]+bv[9][18].z.value[0]+bv[10][19].z.value[0]+bv[11][20].z.value[0]+bv[12][21].z.value[0]+bv[13][22].z.value[0]+bv[14][23].z.value[0]+bv[15][24].z.value[0]+bv[16][25].z.value[0]+bv[17][26].z.value[0]+bv[18][27].z.value[0]+bv[19][28].z.value[0]+bv[20][29].z.value[0]+bv[21][30].z.value[0] == 5,
bv[1][9].z.value[0]+bv[2][10].z.value[0]+bv[3][11].z.value[0]+bv[4][12].z.value[0]+bv[5][13].z.value[0]+bv[6][14].z.value[0]+bv[7][15].z.value[0]+bv[8][16].z.value[0]+bv[9][17].z.value[0]+bv[10][18].z.value[0]+bv[11][19].z.value[0]+bv[12][20].z.value[0]+bv[13][21].z.value[0]+bv[14][22].z.value[0]+bv[15][23].z.value[0]+bv[16][24].z.value[0]+bv[17][25].z.value[0]+bv[18][26].z.value[0]+bv[19][27].z.value[0]+bv[20][28].z.value[0]+bv[21][29].z.value[0]+bv[22][30].z.value[0] == 4,
bv[1][8].z.value[0]+bv[2][9].z.value[0]+bv[3][10].z.value[0]+bv[4][11].z.value[0]+bv[5][12].z.value[0]+bv[6][13].z.value[0]+bv[7][14].z.value[0]+bv[8][15].z.value[0]+bv[9][16].z.value[0]+bv[10][17].z.value[0]+bv[11][18].z.value[0]+bv[12][19].z.value[0]+bv[13][20].z.value[0]+bv[14][21].z.value[0]+bv[15][22].z.value[0]+bv[16][23].z.value[0]+bv[17][24].z.value[0]+bv[18][25].z.value[0]+bv[19][26].z.value[0]+bv[20][27].z.value[0]+bv[21][28].z.value[0]+bv[22][29].z.value[0]+bv[23][30].z.value[0] == 4,
bv[1][7].z.value[0]+bv[2][8].z.value[0]+bv[3][9].z.value[0]+bv[4][10].z.value[0]+bv[5][11].z.value[0]+bv[6][12].z.value[0]+bv[7][13].z.value[0]+bv[8][14].z.value[0]+bv[9][15].z.value[0]+bv[10][16].z.value[0]+bv[11][17].z.value[0]+bv[12][18].z.value[0]+bv[13][19].z.value[0]+bv[14][20].z.value[0]+bv[15][21].z.value[0]+bv[16][22].z.value[0]+bv[17][23].z.value[0]+bv[18][24].z.value[0]+bv[19][25].z.value[0]+bv[20][26].z.value[0]+bv[21][27].z.value[0]+bv[22][28].z.value[0]+bv[23][29].z.value[0]+bv[24][30].z.value[0] == 6,
bv[1][6].z.value[0]+bv[2][7].z.value[0]+bv[3][8].z.value[0]+bv[4][9].z.value[0]+bv[5][10].z.value[0]+bv[6][11].z.value[0]+bv[7][12].z.value[0]+bv[8][13].z.value[0]+bv[9][14].z.value[0]+bv[10][15].z.value[0]+bv[11][16].z.value[0]+bv[12][17].z.value[0]+bv[13][18].z.value[0]+bv[14][19].z.value[0]+bv[15][20].z.value[0]+bv[16][21].z.value[0]+bv[17][22].z.value[0]+bv[18][23].z.value[0]+bv[19][24].z.value[0]+bv[20][25].z.value[0]+bv[21][26].z.value[0]+bv[22][27].z.value[0]+bv[23][28].z.value[0]+bv[24][29].z.value[0]+bv[25][30].z.value[0] == 9,
bv[1][5].z.value[0]+bv[2][6].z.value[0]+bv[3][7].z.value[0]+bv[4][8].z.value[0]+bv[5][9].z.value[0]+bv[6][10].z.value[0]+bv[7][11].z.value[0]+bv[8][12].z.value[0]+bv[9][13].z.value[0]+bv[10][14].z.value[0]+bv[11][15].z.value[0]+bv[12][16].z.value[0]+bv[13][17].z.value[0]+bv[14][18].z.value[0]+bv[15][19].z.value[0]+bv[16][20].z.value[0]+bv[17][21].z.value[0]+bv[18][22].z.value[0]+bv[19][23].z.value[0]+bv[20][24].z.value[0]+bv[21][25].z.value[0]+bv[22][26].z.value[0]+bv[23][27].z.value[0]+bv[24][28].z.value[0]+bv[25][29].z.value[0] == 8,
bv[1][4].z.value[0]+bv[2][5].z.value[0]+bv[3][6].z.value[0]+bv[4][7].z.value[0]+bv[5][8].z.value[0]+bv[6][9].z.value[0]+bv[7][10].z.value[0]+bv[8][11].z.value[0]+bv[9][12].z.value[0]+bv[10][13].z.value[0]+bv[11][14].z.value[0]+bv[12][15].z.value[0]+bv[13][16].z.value[0]+bv[14][17].z.value[0]+bv[15][18].z.value[0]+bv[16][19].z.value[0]+bv[17][20].z.value[0]+bv[18][21].z.value[0]+bv[19][22].z.value[0]+bv[20][23].z.value[0]+bv[21][24].z.value[0]+bv[22][25].z.value[0]+bv[23][26].z.value[0]+bv[24][27].z.value[0]+bv[25][28].z.value[0] == 3,
bv[1][3].z.value[0]+bv[2][4].z.value[0]+bv[3][5].z.value[0]+bv[4][6].z.value[0]+bv[5][7].z.value[0]+bv[6][8].z.value[0]+bv[7][9].z.value[0]+bv[8][10].z.value[0]+bv[9][11].z.value[0]+bv[10][12].z.value[0]+bv[11][13].z.value[0]+bv[12][14].z.value[0]+bv[13][15].z.value[0]+bv[14][16].z.value[0]+bv[15][17].z.value[0]+bv[16][18].z.value[0]+bv[17][19].z.value[0]+bv[18][20].z.value[0]+bv[19][21].z.value[0]+bv[20][22].z.value[0]+bv[21][23].z.value[0]+bv[22][24].z.value[0]+bv[23][25].z.value[0]+bv[24][26].z.value[0]+bv[25][27].z.value[0] == 4,
bv[1][2].z.value[0]+bv[2][3].z.value[0]+bv[3][4].z.value[0]+bv[4][5].z.value[0]+bv[5][6].z.value[0]+bv[6][7].z.value[0]+bv[7][8].z.value[0]+bv[8][9].z.value[0]+bv[9][10].z.value[0]+bv[10][11].z.value[0]+bv[11][12].z.value[0]+bv[12][13].z.value[0]+bv[13][14].z.value[0]+bv[14][15].z.value[0]+bv[15][16].z.value[0]+bv[16][17].z.value[0]+bv[17][18].z.value[0]+bv[18][19].z.value[0]+bv[19][20].z.value[0]+bv[20][21].z.value[0]+bv[21][22].z.value[0]+bv[22][23].z.value[0]+bv[23][24].z.value[0]+bv[24][25].z.value[0]+bv[25][26].z.value[0] == 2,
bv[1][1].z.value[0]+bv[2][2].z.value[0]+bv[3][3].z.value[0]+bv[4][4].z.value[0]+bv[5][5].z.value[0]+bv[6][6].z.value[0]+bv[7][7].z.value[0]+bv[8][8].z.value[0]+bv[9][9].z.value[0]+bv[10][10].z.value[0]+bv[11][11].z.value[0]+bv[12][12].z.value[0]+bv[13][13].z.value[0]+bv[14][14].z.value[0]+bv[15][15].z.value[0]+bv[16][16].z.value[0]+bv[17][17].z.value[0]+bv[18][18].z.value[0]+bv[19][19].z.value[0]+bv[20][20].z.value[0]+bv[21][21].z.value[0]+bv[22][22].z.value[0]+bv[23][23].z.value[0]+bv[24][24].z.value[0]+bv[25][25].z.value[0] == 4,
bv[2][1].z.value[0]+bv[3][2].z.value[0]+bv[4][3].z.value[0]+bv[5][4].z.value[0]+bv[6][5].z.value[0]+bv[7][6].z.value[0]+bv[8][7].z.value[0]+bv[9][8].z.value[0]+bv[10][9].z.value[0]+bv[11][10].z.value[0]+bv[12][11].z.value[0]+bv[13][12].z.value[0]+bv[14][13].z.value[0]+bv[15][14].z.value[0]+bv[16][15].z.value[0]+bv[17][16].z.value[0]+bv[18][17].z.value[0]+bv[19][18].z.value[0]+bv[20][19].z.value[0]+bv[21][20].z.value[0]+bv[22][21].z.value[0]+bv[23][22].z.value[0]+bv[24][23].z.value[0]+bv[25][24].z.value[0] == 7,
bv[3][1].z.value[0]+bv[4][2].z.value[0]+bv[5][3].z.value[0]+bv[6][4].z.value[0]+bv[7][5].z.value[0]+bv[8][6].z.value[0]+bv[9][7].z.value[0]+bv[10][8].z.value[0]+bv[11][9].z.value[0]+bv[12][10].z.value[0]+bv[13][11].z.value[0]+bv[14][12].z.value[0]+bv[15][13].z.value[0]+bv[16][14].z.value[0]+bv[17][15].z.value[0]+bv[18][16].z.value[0]+bv[19][17].z.value[0]+bv[20][18].z.value[0]+bv[21][19].z.value[0]+bv[22][20].z.value[0]+bv[23][21].z.value[0]+bv[24][22].z.value[0]+bv[25][23].z.value[0] == 7,
bv[4][1].z.value[0]+bv[5][2].z.value[0]+bv[6][3].z.value[0]+bv[7][4].z.value[0]+bv[8][5].z.value[0]+bv[9][6].z.value[0]+bv[10][7].z.value[0]+bv[11][8].z.value[0]+bv[12][9].z.value[0]+bv[13][10].z.value[0]+bv[14][11].z.value[0]+bv[15][12].z.value[0]+bv[16][13].z.value[0]+bv[17][14].z.value[0]+bv[18][15].z.value[0]+bv[19][16].z.value[0]+bv[20][17].z.value[0]+bv[21][18].z.value[0]+bv[22][19].z.value[0]+bv[23][20].z.value[0]+bv[24][21].z.value[0]+bv[25][22].z.value[0] == 6,
bv[5][1].z.value[0]+bv[6][2].z.value[0]+bv[7][3].z.value[0]+bv[8][4].z.value[0]+bv[9][5].z.value[0]+bv[10][6].z.value[0]+bv[11][7].z.value[0]+bv[12][8].z.value[0]+bv[13][9].z.value[0]+bv[14][10].z.value[0]+bv[15][11].z.value[0]+bv[16][12].z.value[0]+bv[17][13].z.value[0]+bv[18][14].z.value[0]+bv[19][15].z.value[0]+bv[20][16].z.value[0]+bv[21][17].z.value[0]+bv[22][18].z.value[0]+bv[23][19].z.value[0]+bv[24][20].z.value[0]+bv[25][21].z.value[0] == 7,
bv[6][1].z.value[0]+bv[7][2].z.value[0]+bv[8][3].z.value[0]+bv[9][4].z.value[0]+bv[10][5].z.value[0]+bv[11][6].z.value[0]+bv[12][7].z.value[0]+bv[13][8].z.value[0]+bv[14][9].z.value[0]+bv[15][10].z.value[0]+bv[16][11].z.value[0]+bv[17][12].z.value[0]+bv[18][13].z.value[0]+bv[19][14].z.value[0]+bv[20][15].z.value[0]+bv[21][16].z.value[0]+bv[22][17].z.value[0]+bv[23][18].z.value[0]+bv[24][19].z.value[0]+bv[25][20].z.value[0] == 11,
bv[7][1].z.value[0]+bv[8][2].z.value[0]+bv[9][3].z.value[0]+bv[10][4].z.value[0]+bv[11][5].z.value[0]+bv[12][6].z.value[0]+bv[13][7].z.value[0]+bv[14][8].z.value[0]+bv[15][9].z.value[0]+bv[16][10].z.value[0]+bv[17][11].z.value[0]+bv[18][12].z.value[0]+bv[19][13].z.value[0]+bv[20][14].z.value[0]+bv[21][15].z.value[0]+bv[22][16].z.value[0]+bv[23][17].z.value[0]+bv[24][18].z.value[0]+bv[25][19].z.value[0] == 6,
bv[8][1].z.value[0]+bv[9][2].z.value[0]+bv[10][3].z.value[0]+bv[11][4].z.value[0]+bv[12][5].z.value[0]+bv[13][6].z.value[0]+bv[14][7].z.value[0]+bv[15][8].z.value[0]+bv[16][9].z.value[0]+bv[17][10].z.value[0]+bv[18][11].z.value[0]+bv[19][12].z.value[0]+bv[20][13].z.value[0]+bv[21][14].z.value[0]+bv[22][15].z.value[0]+bv[23][16].z.value[0]+bv[24][17].z.value[0]+bv[25][18].z.value[0] == 6,
bv[9][1].z.value[0]+bv[10][2].z.value[0]+bv[11][3].z.value[0]+bv[12][4].z.value[0]+bv[13][5].z.value[0]+bv[14][6].z.value[0]+bv[15][7].z.value[0]+bv[16][8].z.value[0]+bv[17][9].z.value[0]+bv[18][10].z.value[0]+bv[19][11].z.value[0]+bv[20][12].z.value[0]+bv[21][13].z.value[0]+bv[22][14].z.value[0]+bv[23][15].z.value[0]+bv[24][16].z.value[0]+bv[25][17].z.value[0] == 4,
bv[10][1].z.value[0]+bv[11][2].z.value[0]+bv[12][3].z.value[0]+bv[13][4].z.value[0]+bv[14][5].z.value[0]+bv[15][6].z.value[0]+bv[16][7].z.value[0]+bv[17][8].z.value[0]+bv[18][9].z.value[0]+bv[19][10].z.value[0]+bv[20][11].z.value[0]+bv[21][12].z.value[0]+bv[22][13].z.value[0]+bv[23][14].z.value[0]+bv[24][15].z.value[0]+bv[25][16].z.value[0] == 5,
bv[11][1].z.value[0]+bv[12][2].z.value[0]+bv[13][3].z.value[0]+bv[14][4].z.value[0]+bv[15][5].z.value[0]+bv[16][6].z.value[0]+bv[17][7].z.value[0]+bv[18][8].z.value[0]+bv[19][9].z.value[0]+bv[20][10].z.value[0]+bv[21][11].z.value[0]+bv[22][12].z.value[0]+bv[23][13].z.value[0]+bv[24][14].z.value[0]+bv[25][15].z.value[0] == 7,
bv[12][1].z.value[0]+bv[13][2].z.value[0]+bv[14][3].z.value[0]+bv[15][4].z.value[0]+bv[16][5].z.value[0]+bv[17][6].z.value[0]+bv[18][7].z.value[0]+bv[19][8].z.value[0]+bv[20][9].z.value[0]+bv[21][10].z.value[0]+bv[22][11].z.value[0]+bv[23][12].z.value[0]+bv[24][13].z.value[0]+bv[25][14].z.value[0] == 6,
bv[13][1].z.value[0]+bv[14][2].z.value[0]+bv[15][3].z.value[0]+bv[16][4].z.value[0]+bv[17][5].z.value[0]+bv[18][6].z.value[0]+bv[19][7].z.value[0]+bv[20][8].z.value[0]+bv[21][9].z.value[0]+bv[22][10].z.value[0]+bv[23][11].z.value[0]+bv[24][12].z.value[0]+bv[25][13].z.value[0] == 4,
bv[14][1].z.value[0]+bv[15][2].z.value[0]+bv[16][3].z.value[0]+bv[17][4].z.value[0]+bv[18][5].z.value[0]+bv[19][6].z.value[0]+bv[20][7].z.value[0]+bv[21][8].z.value[0]+bv[22][9].z.value[0]+bv[23][10].z.value[0]+bv[24][11].z.value[0]+bv[25][12].z.value[0] == 6,
bv[15][1].z.value[0]+bv[16][2].z.value[0]+bv[17][3].z.value[0]+bv[18][4].z.value[0]+bv[19][5].z.value[0]+bv[20][6].z.value[0]+bv[21][7].z.value[0]+bv[22][8].z.value[0]+bv[23][9].z.value[0]+bv[24][10].z.value[0]+bv[25][11].z.value[0] == 4,
bv[16][1].z.value[0]+bv[17][2].z.value[0]+bv[18][3].z.value[0]+bv[19][4].z.value[0]+bv[20][5].z.value[0]+bv[21][6].z.value[0]+bv[22][7].z.value[0]+bv[23][8].z.value[0]+bv[24][9].z.value[0]+bv[25][10].z.value[0] == 5,
bv[17][1].z.value[0]+bv[18][2].z.value[0]+bv[19][3].z.value[0]+bv[20][4].z.value[0]+bv[21][5].z.value[0]+bv[22][6].z.value[0]+bv[23][7].z.value[0]+bv[24][8].z.value[0]+bv[25][9].z.value[0] == 1,
bv[18][1].z.value[0]+bv[19][2].z.value[0]+bv[20][3].z.value[0]+bv[21][4].z.value[0]+bv[22][5].z.value[0]+bv[23][6].z.value[0]+bv[24][7].z.value[0]+bv[25][8].z.value[0] == 0,
bv[19][1].z.value[0]+bv[20][2].z.value[0]+bv[21][3].z.value[0]+bv[22][4].z.value[0]+bv[23][5].z.value[0]+bv[24][6].z.value[0]+bv[25][7].z.value[0] == 0,
bv[20][1].z.value[0]+bv[21][2].z.value[0]+bv[22][3].z.value[0]+bv[23][4].z.value[0]+bv[24][5].z.value[0]+bv[25][6].z.value[0] == 0,
bv[21][1].z.value[0]+bv[22][2].z.value[0]+bv[23][3].z.value[0]+bv[24][4].z.value[0]+bv[25][5].z.value[0] == 0,
bv[22][1].z.value[0]+bv[23][2].z.value[0]+bv[24][3].z.value[0]+bv[25][4].z.value[0] == 0,
bv[23][1].z.value[0]+bv[24][2].z.value[0]+bv[25][3].z.value[0] == 0,
bv[24][1].z.value[0]+bv[25][2].z.value[0] == 0,
bv[25][1].z.value[0] == 0,
]
print(len(constraints))
print(len(constraints) - sum(constraints))
print(obj)
